Theorem albii 1819

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 1818	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
2		albii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1797	1 ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓)

Syntax hints:   ↔ wb 206  ∀wal 1538

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  2albii  1820  3albii  1821  hbxfrbi  1825  alex  1826  2nalexn  1828  2exnaln  1829  imnang  1842  alexn  1845  19.26-2  1871  19.26-3an  1872  19.43OLD  1883  albiim  1889  2albiim  1890  empty  1906  19.32v  1940  19.31v  1941  19.23vv  1943  pm11.53v  1944  19.12vvv  1994  equsalvw  2004  2sb6  2087  sbrimvw  2092  sbbiiev  2093  alrot3  2161  alrot4  2162  sbal  2170  sbalv  2171  19.21-2  2210  19.32  2234  19.31  2235  equsalv  2268  sbn  2280  sbrim  2304  sbnfOLD  2312  aaan  2331  pm11.53  2344  19.12vv  2345  sb8v  2351  sb8f  2352  cbvsbvf  2361  equsal  2415  2sb6rf  2471  sbcom3  2504  sb8eulem  2591  eu1  2603  2mo2  2640  2eu1  2644  2eu1v  2645  2eu3  2647  euae  2653  nulmo  2706  eqabbw  2802  hblem  2859  hblemg  2860  eqabbOLD  2868  eqabcb  2869  nfceqi  2888  eqabf  2921  ralbii2  3071  r2allem  3117  r3al  3167  r19.21t  3223  r19.23t  3225  ralcom4  3255  cbvralsvw  3281  sbralie  3317  sbralieOLD  3319  rabbi  3427  rabid2f  3428  rabid2im  3429  eqv  3448  eqvf  3449  abv  3450  abvALT  3451  ralv  3465  ceqsralt  3473  ceqsal  3476  ceqsalv  3478  rspc2gv  3589  ralxpxfr2d  3603  clel2g  3616  clel4g  3620  elabgtOLDOLD  3631  ralab  3655  ralrab2  3660  euind  3686  reu2  3687  reu3  3689  rmo4  3692  reu8  3695  rmo3f  3696  rmoim  3702  2reuswap  3708  2reuswap2  3709  reuind  3715  2reu5lem2  3718  2reu5lem3  3719  2rmoswap  3723  sbccomlem  3823  rmo2  3841  rmo3  3843  rmoanim  3848  dfss2  3923  ss2ab  4016  ss2rab  4024  rabss  4025  uniiunlem  4040  dfdif3OLD  4071  ssequn1  4139  unss  4143  ralunb  4150  ssin  4192  vn0  4298  eq0f  4300  eq0  4303  eq0ALT  4304  ssdif0  4319  inssdif0  4327  ab0w  4332  ab0  4333  ab0ALT  4334  ab0orv  4336  eq0rdv  4360  disj  4403  disj3  4407  ssundif  4441  ralidmw  4461  ralidm  4465  ralf0  4467  pwss  4576  rabsssn  4622  rabeqsnd  4623  ralsnsg  4624  ralsng  4629  disjsn  4665  snssb  4736  snssgOLD  4738  pwpw0  4767  dfnfc2  4883  unissb  4893  elintrab  4913  ssintrab  4924  intun  4933  intprg  4934  dfiin2g  4984  iunssf  4996  iunss  4997  dfdisj2  5064  cbvdisj  5072  cbvdisjv  5073  disjor  5077  dftr2  5204  dftr5  5206  axrep1  5222  axrep4v  5226  axrep4  5227  axrep5  5229  axrep6  5230  axrep6OLD  5231  axsepgfromrep  5236  axnulALT  5246  vnex  5256  inex1  5259  axpweq  5293  zfpow  5308  axpow2  5309  nfnid  5317  dtruALT  5330  reusv2lem4  5343  zfpair2  5375  el  5384  ssextss  5400  moabex  5406  dffr6  5579  dffr2  5584  dffr2ALT  5585  dfepfr  5607  frinxp  5706  ssrel2  5732  eqrelrel  5744  reliun  5763  raliunxp  5786  relop  5797  dmopab3  5866  dm0rn0  5871  reldm0  5874  rnopab3  5902  iresn0n0  6009  dffr3  6054  cotrg  6064  idrefALT  6066  asymref  6069  asymref2  6070  intirr  6071  dffr4  6272  sucel  6387  sb8iota  6453  dffun6  6497  dffun3  6498  dffun4  6499  dffun5  6500  dffun6f  6501  dffun7  6513  funopab  6521  funcnv2  6554  funcnv  6555  fun2cnv  6557  fun11  6560  fununi  6561  fnres  6613  mptfnf  6621  fnopabg  6623  brprcneu  6816  brprcneuALT  6817  dffv2  6922  fvn0ssdmfun  7012  dff13  7195  fnssintima  7303  eqoprab2bw  7423  eqoprab2b  7424  mpo2eqb  7485  ralrnmpo  7492  imaeqalov  7592  zfun  7676  uniex2  7678  funcnvuni  7872  ralxp3f  8077  frpoins3xpg  8080  frpoins3xp3g  8081  xpord3inddlem  8094  dfer2  8633  fiint  9235  fiintOLD  9236  marypha1lem  9342  marypha2lem3  9346  inf2  9538  axinf2  9555  ttrclss  9635  scottexs  9802  scott0s  9803  aceq1  10030  dfac4  10035  dfac7  10046  dfac0  10047  dfac1  10048  dfac10  10051  dfac10c  10052  dfac10b  10053  kmlem4  10067  kmlem12  10075  kmlem14  10077  kmlem15  10078  kmlem16  10079  dfackm  10080  ac6n  10398  axpowndlem3  10512  zfcndrep  10527  zfcndun  10528  zfcndpow  10529  axgroth5  10737  axgroth2  10738  axgroth4  10745  grothprim  10747  sstskm  10755  fimaxre3  12090  infm3  12103  nnwos  12835  cotr2g  14902  brtrclfv  14928  trclfvcotr  14935  rpnnen2lem12  16153  isprm2  16612  vdwmc2  16910  pgpfac1  19980  pgpfac  19984  iunocv  21607  2ndcdisj2  23361  hausdiag  23549  rnelfmlem  23856  alexsubALTlem3  23953  cnextfun  23968  itg2leub  25652  eqscut2  27736  addsuniflem  27932  mulsuniflem  28076  onsfi  28271  mptelee  28859  nmoubi  30735  nmobndseqi  30742  nmobndseqiALT  30743  isch2  31186  isch3  31204  choc0  31289  nmopub  31871  nmfnleub  31888  xfree2  32408  mo5f  32452  nmo  32453  reuxfrdf  32454  rabsspr  32464  rabsstp  32465  inpr0  32495  cbvdisjf  32534  disjorf  32542  ssrelf  32579  funcnvmpt  32629  funcnv5mpt  32630  ssdifidlprm  33414  ballotlem2  34476  bnj89  34707  bnj115  34711  bnj1143  34776  bnj110  34844  bnj611  34904  bnj864  34908  bnj865  34909  bnj1000  34927  bnj978  34935  bnj1049  34960  bnj1052  34961  bnj1090  34965  bnj1030  34973  bnj1133  34975  bnj1171  34986  bnj1172  34987  bnj1174  34989  bnj1176  34991  bnj1204  34998  bnj1253  35003  bnj1388  35019  bnj1523  35057  axreg  35081  axregscl  35082  fineqvrep  35089  fineqvpow  35090  axregs  35093  vonf1owev  35100  axrepprim  35694  axunprim  35695  axpowprim  35696  axinfprim  35698  axacprim  35699  untuni  35701  dffr5  35746  elintfv  35757  dfon2lem8  35783  dfon2lem9  35784  19.12b  35794  brtxpsd3  35889  dfom5b  35905  dffun10  35907  disjeq1i  36185  ss-ax8  36218  cbvdisjvw2  36228  bj-notalbii  36607  bj-ssbeq  36646  bj-ax12ssb  36651  bj-hbext  36703  bj-nfalt  36704  bj-substax12  36714  bj-nnfalt  36759  bj-nnfext  36760  ax11-pm2  36829  bj-sblem  36837  eliminable-veqab  36859  eliminable-abeqv  36860  eliminable-abeqab  36861  bj-ralvw  36872  bj-sbeq  36894  bj-nfcf  36916  bj-snsetex  36956  bj-rcleqf  37018  bj-clex  37024  fvineqsneq  37405  wl-equsalvw  37531  wl-equsalcom  37536  wl-sb9v  37542  wl-sb8eft  37544  wl-sb8et  37546  wl-2sb6d  37551  wl-alanbii  37562  wl-sb8eut  37571  wl-sb8eutv  37572  poimirlem25  37644  poimirlem30  37649  heibor1lem  37808  sbcalfi  38115  mpobi123f  38161  mptbi12f  38165  ineccnvmo  38344  alrmomorn  38345  cocossss  38432  cossssid3  38465  cossssid4  38466  cosscnvssid4  38473  trcoss2  38480  dfeldisj4  38717  dfeldisj5  38718  disjres  38741  dvelimf-o  38927  axc11n-16  38936  pmapglbx  39768  sn-axrep5v  42209  abbibw  42670  dford4  43022  unielss  43211  onsupmaxb  43232  rp-fakeinunass  43508  rababg  43567  elmapintrab  43569  elinintrab  43570  undmrnresiss  43597  clss2lem  43604  cotrintab  43607  elintima  43646  relexp0eq  43694  dfhe3  43768  snhesn  43779  psshepw  43781  dffrege76  43932  frege77  43933  frege110  43966  dffrege115  43971  frege116  43972  frege118  43974  frege131  43987  ntrneikb  44087  ismnuprim  44287  rr-grothprimbi  44288  ismnushort  44294  rr-grothshortbi  44296  pm10.541  44360  pm10.542  44361  19.21vv  44369  19.31vv  44377  19.28vv  44379  pm11.62  44387  axc11next  44399  pm13.196a  44407  2sbc6g  44408  elnev  44431  hbexgVD  44899  dfac5prim  44984  permaxext  44999  permaxrep  45000  permaxpow  45003  permac8prim  45008  rabssf  45117  sinnpoly  46895  2rexsb  47105  dfich2  47462  ichal  47470  spr0nelg  47480  mo0sn  48820  dffun3f  49687  setrec1lem2  49693  setrec2  49700  setis  49703  alimp-surprise  49785  alimp-no-surprise  49786