Theorem albii 1821

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

Syntax hints:   ↔ wb 206  ∀wal 1540

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  2albii  1822  3albii  1823  hbxfrbi  1827  alex  1828  2nalexn  1830  2exnaln  1831  imnang  1844  alexn  1847  19.26-2  1873  19.26-3an  1874  19.43OLD  1885  albiim  1891  2albiim  1892  empty  1908  19.32v  1942  19.31v  1943  19.23vv  1945  pm11.53v  1946  19.12vvv  1996  equsalvw  2006  2sb6  2092  sbrimvw  2097  sbbiiev  2098  alrot3  2166  alrot4  2167  sbal  2175  sbalv  2176  19.21-2  2217  19.32  2241  19.31  2242  equsalv  2275  sbn  2287  sbrim  2311  sbnfOLD  2319  aaan  2338  pm11.53  2351  19.12vv  2352  sb8v  2358  sb8f  2359  cbvsbvf  2368  equsal  2422  2sb6rf  2478  sbcom3  2511  sb8eulem  2599  eu1  2611  2mo2  2648  2eu1  2652  2eu1v  2653  2eu3  2655  euae  2661  nulmo  2714  eqabbw  2810  eqabcbw  2811  hblem  2868  hblemg  2869  eqabcb  2877  nfceqi  2896  eqabf  2929  ralbii2  3080  r2allem  3126  r3al  3176  r19.21t  3232  r19.23t  3234  ralcom4  3264  cbvralsvw  3289  sbralie  3316  sbralieOLD  3318  rabbi  3420  rabid2f  3421  rabid2im  3422  eqv  3440  eqvf  3441  abv  3442  abvALT  3443  ralv  3457  ceqsralt  3465  ceqsal  3468  ceqsalv  3470  rspc2gv  3575  ralxpxfr2d  3589  clel2g  3602  clel4g  3606  elabgtOLDOLD  3617  ralab  3640  ralrab2  3645  euind  3671  reu2  3672  reu3  3674  rmo4  3677  reu8  3680  rmo3f  3681  rmoim  3687  2reuswap  3693  2reuswap2  3694  reuind  3700  2reu5lem2  3703  2reu5lem3  3704  2rmoswap  3708  sbccomlem  3808  rmo2  3826  rmo3  3828  rmoanim  3833  dfss2  3908  ss2ab  4002  ss2rab  4010  rabss  4011  ss2rabd  4013  uniiunlem  4028  dfdif3OLD  4059  ssequn1  4127  unss  4131  ralunb  4138  ssin  4180  eq0f  4288  eq0  4291  eq0ALT  4292  ssdif0  4307  inssdif0  4315  ab0w  4320  ab0  4321  ab0ALT  4322  ab0orv  4324  disj  4391  disj3  4395  ssundif  4428  ralf0  4438  ralidmw  4457  ralidm  4458  pwss  4565  rabsssn  4613  rabeqsnd  4614  ralsnsg  4615  ralsng  4620  disjsn  4656  snssb  4727  pwpw0  4757  dfnfc2  4873  unissb  4884  elintrab  4903  ssintrab  4914  intun  4923  intprg  4924  dfiin2g  4974  iunssf  4986  iunssfOLD  4987  iunss  4988  iunssOLD  4989  dfdisj2  5055  cbvdisj  5063  cbvdisjv  5064  disjor  5068  dftr2  5195  dftr5  5197  axrep1  5213  axrep4v  5217  axrep4  5218  axrep5  5220  axrep6  5221  axrep6OLD  5222  zfrep6  5224  axsepgfromrep  5229  axnulALT  5239  vnex  5251  inex1  5254  axpweq  5288  zfpow  5303  axpow2  5304  nfnid  5312  dtruALT  5325  reusv2lem4  5338  zfpair2  5371  prex  5375  elOLD  5386  ssextss  5400  moabexOLD  5406  dffr6  5580  dffr2  5585  dffr2ALT  5586  dfepfr  5608  frinxp  5707  ssrel2  5734  eqrelrel  5746  raliunxp  5788  relop  5799  dmopab3  5868  dm0rn0  5873  dm0rn0OLD  5874  reldm0  5877  rnopab3  5905  iresn0n0  6013  dffr3  6058  cotrg  6068  idrefALT  6070  asymref  6073  asymref2  6074  intirr  6075  dffr4  6278  sucel  6393  sb8iota  6459  dffun6  6503  dffun3  6504  dffun4  6505  dffun5  6506  dffun6f  6507  dffun7  6519  funopab  6527  funcnv2  6560  funcnv  6561  fun2cnv  6563  fun11  6566  fununi  6567  fnres  6619  mptfnf  6627  fnopabg  6629  tz6.12-2  6821  brprcneu  6824  brprcneuALT  6825  dffv2  6929  funcnvmpt  6943  fvn0ssdmfun  7020  dff13  7202  fnssintima  7310  eqoprab2bw  7430  eqoprab2b  7431  mpo2eqb  7492  ralrnmpo  7499  imaeqalov  7599  zfun  7683  uniex2  7685  funcnvuni  7876  ralxp3f  8080  frpoins3xpg  8083  frpoins3xp3g  8084  xpord3inddlem  8097  dfer2  8637  fiint  9230  marypha1lem  9339  marypha2lem3  9343  inf2  9535  axinf2  9552  ttrclss  9632  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  10513  zfcndrep  10528  zfcndun  10529  zfcndpow  10530  axgroth5  10738  axgroth2  10739  axgroth4  10746  grothprim  10748  sstskm  10756  fimaxre3  12093  infm3  12106  nnwos  12856  cotr2g  14929  brtrclfv  14955  trclfvcotr  14962  rpnnen2lem12  16183  isprm2  16642  vdwmc2  16941  pgpfac1  20048  pgpfac  20052  iunocv  21671  2ndcdisj2  23432  hausdiag  23620  rnelfmlem  23927  alexsubALTlem3  24024  cnextfun  24039  itg2leub  25711  eqcuts2  27792  addsuniflem  28007  mulsuniflem  28155  onsfi  28362  mpteleeOLD  28978  nmoubi  30858  nmobndseqi  30865  nmobndseqiALT  30866  isch2  31309  isch3  31327  choc0  31412  nmopub  31994  nmfnleub  32011  xfree2  32531  mo5f  32573  nmo  32574  reuxfrdf  32575  rabsspr  32586  rabsstp  32587  inpr0  32617  cbvdisjf  32656  disjorf  32664  ssrelf  32703  funcnv5mpt  32755  ssdifidlprm  33533  ballotlem2  34649  bnj89  34880  bnj115  34884  bnj1143  34948  bnj110  35016  bnj611  35076  bnj864  35080  bnj865  35081  bnj1000  35099  bnj978  35107  bnj1049  35132  bnj1052  35133  bnj1090  35137  bnj1030  35145  bnj1133  35147  bnj1171  35158  bnj1172  35159  bnj1174  35161  bnj1176  35163  bnj1204  35170  bnj1253  35175  bnj1388  35191  bnj1523  35229  axnulALT2  35240  fineqvrep  35274  fineqvpow  35275  axreg  35287  axregscl  35288  axregs  35299  vonf1owev  35306  axrepprim  35900  axunprim  35901  axpowprim  35902  axinfprim  35904  axacprim  35905  untuni  35907  dffr5  35952  elintfv  35963  dfon2lem8  35986  dfon2lem9  35987  19.12b  35997  brtxpsd3  36092  dfom5b  36108  dffun10  36110  disjeq1i  36390  ss-ax8  36423  cbvdisjvw2  36433  mh-setind  36734  regsfromregtco  36736  regsfromsetind  36737  regsfromunir1  36738  mh-prprimbi  36741  mh-unprimbi  36742  mh-infprim1bi  36744  mh-infprim2bi  36745  mh-infprim3bi  36746  bj-notalbii  36910  bj-cbvaew  36954  bj-ssbeq  36963  bj-ax12ssb  36968  bj-nfalt  37026  bj-substax12  37037  bj-nnfalt  37103  bj-nnfext  37104  ax11-pm2  37159  bj-sblem  37167  eliminable-veqab  37189  eliminable-abeqv  37190  eliminable-abeqab  37191  bj-ralvw  37202  bj-sbeq  37224  bj-nfcf  37246  bj-snsetex  37286  bj-rcleqf  37348  bj-clex  37354  bj-rep  37396  bj-axseprep  37397  fvineqsneq  37742  wl-equsalvw  37877  wl-equsalcom  37882  wl-sb9v  37888  wl-sb8eft  37890  wl-sb8et  37892  wl-2sb6d  37897  wl-alanbii  37908  wl-sb8eut  37917  wl-sb8eutv  37918  poimirlem25  37980  poimirlem30  37985  heibor1lem  38144  sbcalfi  38451  mpobi123f  38497  mptbi12f  38501  ineccnvmo  38692  alrmomorn  38693  ralmo  38695  ralrmo3  38699  cocossss  38861  cossssid3  38894  cossssid4  38895  cosscnvssid4  38902  trcoss2  38909  dfeldisj4  39147  dfeldisj5  39148  disjres  39179  dvelimf-o  39389  axc11n-16  39398  pmapglbx  40229  sn-axrep5v  42672  abbibw  43124  dford4  43475  unielss  43664  onsupmaxb  43685  rp-fakeinunass  43960  rababg  44019  elmapintrab  44021  elinintrab  44022  undmrnresiss  44049  clss2lem  44056  cotrintab  44059  elintima  44098  relexp0eq  44146  dfhe3  44220  snhesn  44231  psshepw  44233  dffrege76  44384  frege77  44385  frege110  44418  dffrege115  44423  frege116  44424  frege118  44426  frege131  44439  ntrneikb  44539  ismnuprim  44739  rr-grothprimbi  44740  ismnushort  44746  rr-grothshortbi  44748  pm10.541  44812  pm10.542  44813  19.21vv  44821  19.31vv  44829  19.28vv  44831  pm11.62  44839  axc11next  44851  pm13.196a  44859  2sbc6g  44860  elnev  44882  hbexgVD  45350  dfac5prim  45435  permaxext  45450  permaxrep  45451  permaxpow  45454  permac8prim  45459  rabssf  45567  sinnpoly  47351  2rexsb  47561  dfich2  47930  ichal  47938  spr0nelg  47948  mo0sn  49303  dffun3f  50169  setrec1lem2  50175  setrec2  50182  setis  50185  alimp-surprise  50267  alimp-no-surprise  50268