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  12089  infm3  12102  nnwos  12834  cotr2g  14901  brtrclfv  14927  trclfvcotr  14934  rpnnen2lem12  16152  isprm2  16611  vdwmc2  16909  pgpfac1  19979  pgpfac  19983  iunocv  21606  2ndcdisj2  23360  hausdiag  23548  rnelfmlem  23855  alexsubALTlem3  23952  cnextfun  23967  itg2leub  25651  eqscut2  27735  addsuniflem  27931  mulsuniflem  28075  onsfi  28270  mptelee  28858  nmoubi  30734  nmobndseqi  30741  nmobndseqiALT  30742  isch2  31185  isch3  31203  choc0  31288  nmopub  31870  nmfnleub  31887  xfree2  32407  mo5f  32451  nmo  32452  reuxfrdf  32453  rabsspr  32463  rabsstp  32464  inpr0  32494  cbvdisjf  32533  disjorf  32541  ssrelf  32576  funcnvmpt  32624  funcnv5mpt  32625  ssdifidlprm  33405  ballotlem2  34456  bnj89  34687  bnj115  34691  bnj1143  34756  bnj110  34824  bnj611  34884  bnj864  34888  bnj865  34889  bnj1000  34907  bnj978  34915  bnj1049  34940  bnj1052  34941  bnj1090  34945  bnj1030  34953  bnj1133  34955  bnj1171  34966  bnj1172  34967  bnj1174  34969  bnj1176  34971  bnj1204  34978  bnj1253  34983  bnj1388  34999  bnj1523  35037  axreg  35061  axregscl  35062  fineqvrep  35069  fineqvpow  35070  axregs  35073  vonf1owev  35080  axrepprim  35674  axunprim  35675  axpowprim  35676  axinfprim  35678  axacprim  35679  untuni  35681  dffr5  35726  elintfv  35737  dfon2lem8  35763  dfon2lem9  35764  19.12b  35774  brtxpsd3  35869  dfom5b  35885  dffun10  35887  disjeq1i  36165  ss-ax8  36198  cbvdisjvw2  36208  bj-notalbii  36587  bj-ssbeq  36626  bj-ax12ssb  36631  bj-hbext  36683  bj-nfalt  36684  bj-substax12  36694  bj-nnfalt  36739  bj-nnfext  36740  ax11-pm2  36809  bj-sblem  36817  eliminable-veqab  36839  eliminable-abeqv  36840  eliminable-abeqab  36841  bj-ralvw  36852  bj-sbeq  36874  bj-nfcf  36896  bj-snsetex  36936  bj-rcleqf  36998  bj-clex  37004  fvineqsneq  37385  wl-equsalvw  37511  wl-equsalcom  37516  wl-sb9v  37522  wl-sb8eft  37524  wl-sb8et  37526  wl-2sb6d  37531  wl-alanbii  37542  wl-sb8eut  37551  wl-sb8eutv  37552  poimirlem25  37624  poimirlem30  37629  heibor1lem  37788  sbcalfi  38095  mpobi123f  38141  mptbi12f  38145  ineccnvmo  38324  alrmomorn  38325  cocossss  38412  cossssid3  38445  cossssid4  38446  cosscnvssid4  38453  trcoss2  38460  dfeldisj4  38697  dfeldisj5  38698  disjres  38721  dvelimf-o  38907  axc11n-16  38916  pmapglbx  39748  sn-axrep5v  42189  abbibw  42650  dford4  43002  unielss  43191  onsupmaxb  43212  rp-fakeinunass  43488  rababg  43547  elmapintrab  43549  elinintrab  43550  undmrnresiss  43577  clss2lem  43584  cotrintab  43587  elintima  43626  relexp0eq  43674  dfhe3  43748  snhesn  43759  psshepw  43761  dffrege76  43912  frege77  43913  frege110  43946  dffrege115  43951  frege116  43952  frege118  43954  frege131  43967  ntrneikb  44067  ismnuprim  44267  rr-grothprimbi  44268  ismnushort  44274  rr-grothshortbi  44276  pm10.541  44340  pm10.542  44341  19.21vv  44349  19.31vv  44357  19.28vv  44359  pm11.62  44367  axc11next  44379  pm13.196a  44387  2sbc6g  44388  elnev  44411  hbexgVD  44879  dfac5prim  44964  permaxext  44979  permaxrep  44980  permaxpow  44983  permac8prim  44988  rabssf  45097  sinnpoly  46876  2rexsb  47086  dfich2  47443  ichal  47451  spr0nelg  47461  mo0sn  48801  dffun3f  49668  setrec1lem2  49674  setrec2  49681  setis  49684  alimp-surprise  49766  alimp-no-surprise  49767