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  1988  equsalvw  2003  2sb6  2086  sbrimvw  2091  sbbiiev  2092  alrot3  2160  alrot4  2161  sbal  2169  sbalv  2170  19.21-2  2209  19.32  2233  19.31  2234  equsalv  2267  sbn  2280  sbrim  2304  sbnfOLD  2313  aaan  2333  aaanOLD  2334  pm11.53  2348  19.12vv  2349  sb8v  2355  sb8f  2356  cbvsbvf  2366  equsal  2422  2sb6rf  2478  sbcom3  2511  sb8eulem  2598  eu1  2610  2mo2  2647  2eu1  2651  2eu1v  2652  2eu3  2654  euae  2660  nulmo  2713  eqabbw  2815  hblem  2873  hblemg  2874  eqabbOLD  2882  eqabcb  2883  nfceqi  2902  eqabf  2935  ralbii2  3089  r2allem  3142  r19.21vOLD  3181  r3al  3197  r19.21t  3253  r19.23t  3255  ralcom4  3286  ralcom4OLD  3287  nfra2wOLD  3300  cbvralsvw  3317  sbralie  3358  moelOLD  3405  rabbi  3467  rabid2f  3468  rabid2im  3469  rabid2OLD  3471  eqv  3490  eqvf  3491  abv  3492  abvALT  3493  ralv  3508  ceqsralt  3516  ceqsal  3519  ceqsalv  3521  rspc2gv  3632  ralxpxfr2d  3646  clel2g  3659  clel4g  3663  elabgtOLD  3673  elabg  3676  ralab  3697  ralabOLD  3698  ralrab2  3704  euind  3730  reu2  3731  reu3  3733  rmo4  3736  reu8  3739  rmo3f  3740  rmoim  3746  2reuswap  3752  2reuswap2  3753  reuind  3759  2reu5lem2  3762  2reu5lem3  3763  2rmoswap  3767  sbccomlem  3869  rmo2  3887  rmo3  3889  rmoanim  3894  dfss2  3969  ss2ab  4062  ss2rab  4071  rabss  4072  uniiunlem  4087  dfdif3OLD  4118  ssequn1  4186  unss  4190  ralunb  4197  ssin  4239  vn0  4345  eq0f  4347  eq0  4350  eq0ALT  4351  ssdif0  4366  inssdif0  4374  ab0w  4379  ab0  4380  ab0ALT  4381  ab0orv  4383  eq0rdv  4407  disj  4450  disj3  4454  ssundif  4488  ralidmw  4508  ralidm  4512  ralf0  4514  pwss  4623  rabsssn  4668  rabeqsnd  4669  ralsnsg  4670  ralsng  4675  disjsn  4711  snssb  4782  snssgOLD  4784  pwpw0  4813  dfnfc2  4929  unissb  4939  unissbOLD  4940  elintrab  4960  ssintrab  4971  intun  4980  intprg  4981  dfiin2g  5032  iunssf  5044  iunss  5045  dfdisj2  5112  cbvdisj  5120  cbvdisjv  5121  disjor  5125  dftr2  5261  dftr5  5263  dftr5OLD  5264  axrep1  5280  axrep4v  5284  axrep4  5285  axrep5  5287  axrep6  5288  axrep6OLD  5289  axsepgfromrep  5294  axnulALT  5304  vnex  5314  inex1  5317  axpweq  5351  zfpow  5366  axpow2  5367  nfnid  5375  dtruALT  5388  reusv2lem4  5401  zfpair2  5433  el  5442  ssextss  5458  moabex  5464  dffr6  5640  dffr2  5646  dffr2ALT  5647  dfepfr  5669  frinxp  5768  ssrel2  5795  eqrelrel  5807  reliun  5826  raliunxp  5850  relop  5861  dmopab3  5930  dm0rn0  5935  reldm0  5938  rnopab3  5967  iresn0n0  6072  dffr3  6117  cotrg  6127  cotrgOLD  6128  cotrgOLDOLD  6129  idrefALT  6131  asymref  6136  asymref2  6137  intirr  6138  dffr4  6341  sucel  6458  sb8iota  6525  dffun2OLDOLD  6573  dffun6  6574  dffun3  6575  dffun3OLD  6576  dffun4  6577  dffun5  6578  dffun6f  6579  dffun7  6593  funopab  6601  funcnv2  6634  funcnv  6635  fun2cnv  6637  fun11  6640  fununi  6641  fnres  6695  mptfnf  6703  fnopabg  6705  brprcneu  6896  brprcneuALT  6897  dffv2  7004  fvn0ssdmfun  7094  dff13  7275  fnssintima  7382  eqoprab2bw  7503  eqoprab2b  7504  mpo2eqb  7565  ralrnmpo  7572  imaeqalov  7672  zfun  7756  uniex2  7758  funcnvuni  7954  ralxp3f  8162  frpoins3xpg  8165  frpoins3xp3g  8166  xpord3inddlem  8179  dfer2  8746  fiint  9366  fiintOLD  9367  marypha1lem  9473  marypha2lem3  9477  inf2  9663  axinf2  9680  ttrclss  9760  scottexs  9927  scott0s  9928  aceq1  10157  dfac4  10162  dfac7  10173  dfac0  10174  dfac1  10175  dfac10  10178  dfac10c  10179  dfac10b  10180  kmlem4  10194  kmlem12  10202  kmlem14  10204  kmlem15  10205  kmlem16  10206  dfackm  10207  ac6n  10525  axpowndlem3  10639  zfcndrep  10654  zfcndun  10655  zfcndpow  10656  axgroth5  10864  axgroth2  10865  axgroth4  10872  grothprim  10874  sstskm  10882  fimaxre3  12214  infm3  12227  nnwos  12957  cotr2g  15015  brtrclfv  15041  trclfvcotr  15048  rpnnen2lem12  16261  isprm2  16719  vdwmc2  17017  pgpfac1  20100  pgpfac  20104  iunocv  21699  2ndcdisj2  23465  hausdiag  23653  rnelfmlem  23960  alexsubALTlem3  24057  cnextfun  24072  itg2leub  25769  eqscut2  27851  addsuniflem  28034  mulsuniflem  28175  mptelee  28910  nmoubi  30791  nmobndseqi  30798  nmobndseqiALT  30799  isch2  31242  isch3  31260  choc0  31345  nmopub  31927  nmfnleub  31944  xfree2  32464  mo5f  32508  nmo  32509  reuxfrdf  32510  rabsspr  32520  rabsstp  32521  inpr0  32550  cbvdisjf  32584  disjorf  32592  ssrelf  32627  funcnvmpt  32677  funcnv5mpt  32678  ssdifidlprm  33486  ballotlem2  34491  bnj89  34735  bnj115  34739  bnj1143  34804  bnj110  34872  bnj611  34932  bnj864  34936  bnj865  34937  bnj1000  34955  bnj978  34963  bnj1049  34988  bnj1052  34989  bnj1090  34993  bnj1030  35001  bnj1133  35003  bnj1171  35014  bnj1172  35015  bnj1174  35017  bnj1176  35019  bnj1204  35026  bnj1253  35031  bnj1388  35047  bnj1523  35085  fineqvrep  35109  fineqvpow  35110  axrepprim  35702  axunprim  35703  axpowprim  35704  axinfprim  35706  axacprim  35707  untuni  35709  dffr5  35754  elintfv  35765  dfon2lem8  35791  dfon2lem9  35792  19.12b  35802  brtxpsd3  35897  dfom5b  35913  dffun10  35915  disjeq1i  36193  ss-ax8  36226  cbvdisjvw2  36236  bj-notalbii  36615  bj-ssbeq  36654  bj-ax12ssb  36659  bj-hbext  36711  bj-nfalt  36712  bj-substax12  36722  bj-nnfalt  36767  bj-nnfext  36768  ax11-pm2  36837  bj-sblem  36845  eliminable-veqab  36867  eliminable-abeqv  36868  eliminable-abeqab  36869  bj-ralvw  36880  bj-sbeq  36902  bj-nfcf  36924  bj-snsetex  36964  bj-rcleqf  37026  bj-clex  37032  fvineqsneq  37413  wl-equsalvw  37539  wl-equsalcom  37544  wl-sb9v  37550  wl-sb8eft  37552  wl-sb8et  37554  wl-2sb6d  37559  wl-alanbii  37570  wl-sb8eut  37579  wl-sb8eutv  37580  poimirlem25  37652  poimirlem30  37657  heibor1lem  37816  sbcalfi  38123  mpobi123f  38169  mptbi12f  38173  ineccnvmo  38358  alrmomorn  38359  cocossss  38437  cossssid3  38470  cossssid4  38471  cosscnvssid4  38478  trcoss2  38485  dfeldisj4  38721  dfeldisj5  38722  disjres  38745  dvelimf-o  38930  axc11n-16  38939  pmapglbx  39771  sn-axrep5v  42255  abbibw  42687  dford4  43041  unielss  43230  onsupmaxb  43251  rp-fakeinunass  43528  rababg  43587  elmapintrab  43589  elinintrab  43590  undmrnresiss  43617  clss2lem  43624  cotrintab  43627  elintima  43666  relexp0eq  43714  dfhe3  43788  snhesn  43799  psshepw  43801  dffrege76  43952  frege77  43953  frege110  43986  dffrege115  43991  frege116  43992  frege118  43994  frege131  44007  ntrneikb  44107  ismnuprim  44313  rr-grothprimbi  44314  ismnushort  44320  rr-grothshortbi  44322  pm10.541  44386  pm10.542  44387  19.21vv  44395  19.31vv  44403  19.28vv  44405  pm11.62  44413  axc11next  44425  pm13.196a  44433  2sbc6g  44434  elnev  44457  hbexgVD  44926  dfac5prim  45007  rabssf  45124  2rexsb  47113  dfich2  47445  ichal  47453  spr0nelg  47463  mo0sn  48735  dffun3f  49201  setrec1lem2  49207  setrec2  49214  setis  49217  alimp-surprise  49299  alimp-no-surprise  49300