Theorem albii 1814

Description: Inference adding universal quantifier to both sides of an equivalence. (Contributed by NM, 7-Aug-1994.)

Hypothesis

Ref	Expression
albii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
albii	⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓)

Proof of Theorem albii

Step	Hyp	Ref	Expression
1		albi 1813	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
2		albii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1792	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓)

Syntax hints:   ↔ wb 205  ∀wal 1532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  2albii  1815  3albii  1816  hbxfrbi  1820  alex  1821  2nalexn  1823  2exnaln  1824  imnang  1837  alexn  1840  nfnbiOLD  1851  19.26-2  1867  19.26-3an  1868  19.43OLD  1879  albiim  1885  2albiim  1886  empty  1902  19.32v  1936  19.31v  1937  19.23vv  1939  pm11.53v  1940  19.12vvv  1985  equsalvw  2000  2sb6  2082  sbrimvw  2087  sbcom3vv  2091  alrot3  2150  alrot4  2151  sbal  2159  sbalv  2160  19.21-2  2198  19.32  2222  19.31  2223  equsalv  2254  sbn  2270  sbrim  2294  sbnfOLD  2303  aaan  2322  aaanOLD  2323  pm11.53  2337  19.12vv  2338  sb8v  2343  sb8f  2344  cbvsbvf  2355  equsal  2411  2sb6rf  2467  sbcom3  2500  sb8eulem  2587  eu1  2599  2mo2  2636  2eu1  2640  2eu1v  2641  2eu3  2643  euae  2649  nulmo  2702  eqabbw  2802  hblem  2858  hblemg  2859  eqabbOLD  2867  eqabcb  2868  nfceqi  2889  eqabf  2925  ralbii2  3079  r2allem  3132  r19.21vOLD  3171  r3al  3187  r19.21t  3241  r19.23t  3243  ralcom4  3274  ralcom4OLD  3275  nfra2wOLD  3288  sbralie  3342  moelOLD  3389  rabbi  3450  rabid2f  3451  rabid2im  3452  rabid2OLD  3454  eqv  3472  eqvf  3473  abv  3474  abvALT  3475  ralv  3489  ceqsralt  3497  ceqsal  3500  ceqsalv  3502  rspc2gv  3618  ralxpxfr2d  3631  clel2g  3644  clel4g  3649  elabgtOLD  3660  elabg  3664  ralab  3685  ralabOLD  3686  ralrab2  3692  euind  3718  reu2  3719  reu3  3721  rmo4  3724  reu8  3727  rmo3f  3728  rmoim  3734  2reuswap  3740  2reuswap2  3741  reuind  3747  2reu5lem2  3750  2reu5lem3  3751  2rmoswap  3755  rmo2  3880  rmo3  3882  rmoanim  3887  dfss2  3965  ss2ab  4056  ss2rab  4067  rabss  4068  uniiunlem  4083  dfdif3  4113  ssequn1  4181  unss  4185  ralunb  4192  ssin  4232  vn0  4341  eq0f  4343  eq0  4346  eq0ALT  4347  ssdif0  4366  inssdif0  4374  ab0w  4378  ab0  4379  ab0OLD  4380  ab0ALT  4381  ab0orv  4383  eq0rdv  4409  disj  4452  disjOLD  4453  disj3  4458  ssundif  4492  ralidmw  4512  ralidm  4516  ralf0  4518  ralf0OLD  4522  pwss  4630  rabsssn  4675  rabeqsnd  4676  ralsnsg  4677  ralsng  4682  disjsn  4720  snssb  4791  snssgOLD  4793  pwpw0  4822  dfnfc2  4937  unissb  4947  unissbOLD  4948  elintrab  4968  ssintrab  4979  intun  4988  intprg  4989  intprOLD  4991  dfiin2g  5040  iunssf  5052  iunss  5053  dfdisj2  5120  cbvdisj  5128  disjor  5133  dftr2  5272  dftr5  5274  dftr5OLD  5275  axrep1  5291  axrep5  5296  axrep6  5297  axsepgfromrep  5302  axnulALT  5309  vnex  5319  inex1  5322  axpweq  5354  zfpow  5370  axpow2  5371  axpow3  5372  nfnid  5379  dtruALT  5392  reusv2lem4  5405  zfpair2  5434  el  5443  ssextss  5459  moabex  5465  dffr6  5640  dffr2  5646  dffr2ALT  5647  dfepfr  5667  frinxp  5764  ssrel2  5791  eqrelrel  5803  reliun  5822  raliunxp  5846  relop  5857  dmopab3  5926  dm0rn0  5931  reldm0  5934  iresn0n0  6063  dffr3  6109  cotrg  6119  cotrgOLD  6120  cotrgOLDOLD  6121  idrefALT  6123  asymref  6128  asymref2  6129  intirr  6130  dffr4  6332  sucel  6450  sb8iota  6518  dffun2OLDOLD  6566  dffun6  6567  dffun3  6568  dffun3OLD  6569  dffun4  6570  dffun5  6571  dffun6f  6572  dffun7  6586  funopab  6594  funcnv2  6627  funcnv  6628  fun2cnv  6630  fun11  6633  fununi  6634  fnres  6688  mptfnf  6696  fnopabg  6698  brprcneu  6891  brprcneuALT  6892  dffv2  6997  fvn0ssdmfun  7088  dff13  7270  fnssintima  7374  eqoprab2bw  7495  eqoprab2b  7496  mpo2eqb  7558  ralrnmpo  7565  imaeqalov  7665  zfun  7747  uniex2  7749  funcnvuni  7945  ralxp3f  8151  frpoins3xpg  8154  frpoins3xp3g  8155  xpord3inddlem  8168  dfer2  8735  fiint  9368  fiintOLD  9369  marypha1lem  9476  marypha2lem3  9480  inf2  9666  axinf2  9683  ttrclss  9763  scottexs  9930  scott0s  9931  aceq1  10160  dfac4  10165  dfac7  10175  dfac0  10176  dfac1  10177  dfac10  10180  dfac10c  10181  dfac10b  10182  kmlem4  10196  kmlem12  10204  kmlem14  10206  kmlem15  10207  kmlem16  10208  dfackm  10209  ac6n  10528  axpowndlem3  10642  zfcndrep  10657  zfcndun  10658  zfcndpow  10659  axgroth5  10867  axgroth2  10868  axgroth4  10875  grothprim  10877  sstskm  10885  fimaxre3  12212  infm3  12225  nnwos  12951  cotr2g  14981  brtrclfv  15007  trclfvcotr  15014  rpnnen2lem12  16227  isprm2  16683  vdwmc2  16981  pgpfac1  20080  pgpfac  20084  iunocv  21677  2ndcdisj2  23452  hausdiag  23640  rnelfmlem  23947  alexsubALTlem3  24044  cnextfun  24059  itg2leub  25755  eqscut2  27836  addsuniflem  28015  mulsuniflem  28150  mptelee  28829  nmoubi  30705  nmobndseqi  30712  nmobndseqiALT  30713  isch2  31156  isch3  31174  choc0  31259  nmopub  31841  nmfnleub  31858  xfree2  32378  mo5f  32417  nmo  32418  reuxfrdf  32419  inpr0  32458  cbvdisjf  32491  disjorf  32499  ssrelf  32535  funcnvmpt  32584  funcnv5mpt  32585  ssdifidlprm  33333  ballotlem2  34322  bnj89  34566  bnj115  34570  bnj1143  34635  bnj110  34703  bnj611  34763  bnj864  34767  bnj865  34768  bnj1000  34786  bnj978  34794  bnj1049  34819  bnj1052  34820  bnj1090  34824  bnj1030  34832  bnj1133  34834  bnj1171  34845  bnj1172  34846  bnj1174  34848  bnj1176  34850  bnj1204  34857  bnj1253  34862  bnj1388  34878  bnj1523  34916  fineqvrep  34931  fineqvpow  34932  axrepprim  35524  axunprim  35525  axpowprim  35526  axinfprim  35528  axacprim  35529  untuni  35531  dffr5  35576  elintfv  35588  dfon2lem8  35614  dfon2lem9  35615  19.12b  35625  brtxpsd3  35720  dfom5b  35736  dffun10  35738  bj-notalbii  36319  bj-ssbeq  36357  bj-ax12ssb  36362  bj-hbext  36415  bj-nfalt  36416  bj-substax12  36426  bj-nnfalt  36471  bj-nnfext  36472  ax11-pm2  36541  bj-sblem  36549  eliminable-veqab  36571  eliminable-abeqv  36572  eliminable-abeqab  36573  bj-ralvw  36585  bj-sbeq  36607  bj-nfcf  36629  bj-snsetex  36670  bj-rcleqf  36732  bj-clex  36738  fvineqsneq  37119  wl-equsalvw  37233  wl-equsalcom  37238  wl-sb9v  37244  wl-sb8eft  37246  wl-sb8et  37248  wl-2sb6d  37253  wl-alanbii  37264  wl-sb8eut  37273  wl-sb8eutv  37274  poimirlem25  37346  poimirlem30  37351  heibor1lem  37510  sbcalfi  37817  mpobi123f  37863  mptbi12f  37867  ineccnvmo  38055  alrmomorn  38056  cocossss  38134  cossssid3  38167  cossssid4  38168  cosscnvssid4  38175  trcoss2  38182  dfeldisj4  38418  dfeldisj5  38419  disjres  38442  dvelimf-o  38627  axc11n-16  38636  pmapglbx  39468  sn-axrep5v  41938  abbibw  42332  dford4  42687  unielss  42883  onsupmaxb  42904  rp-fakeinunass  43182  rababg  43241  elmapintrab  43243  elinintrab  43244  undmrnresiss  43271  clss2lem  43278  cotrintab  43281  elintima  43320  relexp0eq  43368  dfhe3  43442  snhesn  43453  psshepw  43455  dffrege76  43606  frege77  43607  frege110  43640  dffrege115  43645  frege116  43646  frege118  43648  frege131  43661  ntrneikb  43761  ismnuprim  43968  rr-grothprimbi  43969  ismnushort  43975  rr-grothshortbi  43977  pm10.541  44041  pm10.542  44042  19.21vv  44050  19.31vv  44058  19.28vv  44060  pm11.62  44068  axc11next  44080  pm13.196a  44088  2sbc6g  44089  elnev  44112  hbexgVD  44582  rabssf  44720  2rexsb  46714  dfich2  47030  ichal  47038  spr0nelg  47048  mo0sn  48201  dffun3f  48428  setrec1lem2  48434  setrec2  48441  setis  48444  alimp-surprise  48528  alimp-no-surprise  48529

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »