Theorem albii 1822

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

Syntax hints:   ↔ wb 205  ∀wal 1540

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  2albii  1823  3albii  1824  hbxfrbi  1828  alex  1829  2nalexn  1831  2exnaln  1832  imnang  1845  alexn  1848  nfnbiOLD  1859  19.26-2  1875  19.26-3an  1876  19.43OLD  1887  albiim  1893  2albiim  1894  empty  1910  19.32v  1944  19.31v  1945  19.23vv  1947  pm11.53v  1948  19.12vvv  1993  equsalvw  2008  2sb6  2090  sbrimvw  2095  sbcom3vv  2099  alrot3  2158  alrot4  2159  sbal  2160  sbalv  2161  19.21-2  2203  19.32  2227  19.31  2228  equsalv  2259  sbn  2277  sbrim  2301  aaan  2328  aaanOLD  2329  pm11.53  2343  19.12vv  2344  sb8v  2349  sb8f  2350  cbvsbvf  2361  equsal  2417  2sb6rf  2473  sbcom3  2506  sb8eulem  2593  eu1  2607  2mo2  2644  2eu1  2647  2eu1v  2648  2eu3  2650  euae  2656  nulmo  2709  eqabbw  2810  hblem  2866  hblemg  2867  eqabbOLD  2875  eqabcb  2876  nfcriOLD  2894  nfcriOLDOLD  2895  nfcriiOLD  2897  nfceqi  2901  eqabf  2936  ralbii2  3090  r2allem  3143  r19.21vOLD  3181  r3al  3197  r19.21t  3251  r19.23t  3253  ralcom4  3284  ralcom4OLD  3285  nfra2wOLD  3298  sbralie  3355  moelOLD  3402  rabbi  3463  rabid2f  3464  rabid2OLD  3466  eqv  3484  eqvf  3485  abv  3486  abvALT  3487  ralv  3499  ceqsralt  3507  ceqsal  3510  ceqsalv  3512  rspc2gv  3621  ralxpxfr2d  3634  clel2g  3647  clel4g  3652  elabgt  3662  elabg  3666  ralab  3687  ralabOLD  3688  ralrab2  3694  euind  3720  reu2  3721  reu3  3723  rmo4  3726  reu8  3729  rmo3f  3730  rmoim  3736  2reuswap  3742  2reuswap2  3743  reuind  3749  2reu5lem2  3752  2reu5lem3  3753  2rmoswap  3757  rmo2  3881  rmo3  3883  rmoanim  3888  dfss2  3968  dfss2OLD  3969  ss2ab  4056  ss2rab  4068  rabss  4069  uniiunlem  4084  dfdif3  4114  ssequn1  4180  unss  4184  ralunb  4191  ssin  4230  vn0  4338  eq0f  4340  eq0  4343  eq0ALT  4344  ssdif0  4363  inssdif0  4369  ab0w  4373  ab0  4374  ab0OLD  4375  ab0ALT  4376  ab0orv  4378  eq0rdv  4404  disj  4447  disjOLD  4448  disj3  4453  ssundif  4487  ralidmw  4507  ralidm  4511  ralf0  4513  ralf0OLD  4517  pwss  4625  rabsssn  4670  rabeqsnd  4671  ralsnsg  4672  ralsng  4677  disjsn  4715  snssb  4786  snssgOLD  4788  pwpw0  4816  pwsnOLD  4901  dfnfc2  4933  unissb  4943  unissbOLD  4944  elintrab  4964  ssintrab  4975  intun  4984  intprg  4985  intprOLD  4987  dfiin2g  5035  iunssf  5047  iunss  5048  dfdisj2  5115  cbvdisj  5123  disjor  5128  dftr2  5267  dftr5  5269  dftr5OLD  5270  axrep1  5286  axrep5  5291  axrep6  5292  axsepgfromrep  5297  axnulALT  5304  vnex  5314  inex1  5317  axpweq  5348  zfpow  5364  axpow2  5365  axpow3  5366  nfnid  5373  dtruALT  5386  reusv2lem4  5399  zfpair2  5428  el  5437  ssextss  5453  moabex  5459  dffr6  5634  dffr2  5640  dffr2ALT  5641  dfepfr  5661  frinxp  5757  ssrel2  5784  eqrelrel  5796  reliun  5815  raliunxp  5838  relop  5849  dmopab3  5918  dm0rn0  5923  reldm0  5926  iresn0n0  6052  dffr3  6096  cotrg  6106  cotrgOLD  6107  cotrgOLDOLD  6108  idrefALT  6110  asymref  6115  asymref2  6116  intirr  6117  dffr4  6318  sucel  6436  sb8iota  6505  dffun2OLDOLD  6553  dffun6  6554  dffun3  6555  dffun3OLD  6556  dffun4  6557  dffun5  6558  dffun6f  6559  dffun7  6573  funopab  6581  funcnv2  6614  funcnv  6615  fun2cnv  6617  fun11  6620  fununi  6621  fnres  6675  mptfnf  6683  fnopabg  6685  brprcneu  6879  brprcneuALT  6880  dffv2  6984  fvn0ssdmfun  7074  dff13  7251  fnssintima  7356  eqoprab2bw  7476  eqoprab2b  7477  mpo2eqb  7538  ralrnmpo  7544  imaeqalov  7643  zfun  7723  uniex2  7725  funcnvuni  7919  ralxp3f  8120  frpoins3xpg  8123  frpoins3xp3g  8124  xpord3inddlem  8137  dfer2  8701  fiint  9321  marypha1lem  9425  marypha2lem3  9429  inf2  9615  axinf2  9632  ttrclss  9712  scottexs  9879  scott0s  9880  aceq1  10109  dfac4  10114  dfac7  10124  dfac0  10125  dfac1  10126  dfac10  10129  dfac10c  10130  dfac10b  10131  kmlem4  10145  kmlem12  10153  kmlem14  10155  kmlem15  10156  kmlem16  10157  dfackm  10158  ac6n  10477  axpowndlem3  10591  zfcndrep  10606  zfcndun  10607  zfcndpow  10608  axgroth5  10816  axgroth2  10817  axgroth4  10824  grothprim  10826  sstskm  10834  fimaxre3  12157  infm3  12170  nnwos  12896  cotr2g  14920  brtrclfv  14946  trclfvcotr  14953  rpnnen2lem12  16165  isprm2  16616  vdwmc2  16909  pgpfac1  19945  pgpfac  19949  iunocv  21226  2ndcdisj2  22953  hausdiag  23141  rnelfmlem  23448  alexsubALTlem3  23545  cnextfun  23560  itg2leub  25244  eqscut2  27297  addsuniflem  27474  mulsuniflem  27594  mptelee  28143  nmoubi  30013  nmobndseqi  30020  nmobndseqiALT  30021  isch2  30464  isch3  30482  choc0  30567  nmopub  31149  nmfnleub  31166  xfree2  31686  mo5f  31717  nmo  31718  reuxfrdf  31719  inpr0  31757  cbvdisjf  31790  disjorf  31798  ssrelf  31832  funcnvmpt  31880  funcnv5mpt  31881  ballotlem2  33476  bnj89  33721  bnj115  33725  bnj1143  33790  bnj110  33858  bnj611  33918  bnj864  33922  bnj865  33923  bnj1000  33941  bnj978  33949  bnj1049  33974  bnj1052  33975  bnj1090  33979  bnj1030  33987  bnj1133  33989  bnj1171  34000  bnj1172  34001  bnj1174  34003  bnj1176  34005  bnj1204  34012  bnj1253  34017  bnj1388  34033  bnj1523  34071  fineqvrep  34084  fineqvpow  34085  axrepprim  34660  axunprim  34661  axpowprim  34662  axinfprim  34664  axacprim  34665  untuni  34667  dffr5  34713  elintfv  34725  dfon2lem8  34751  dfon2lem9  34752  19.12b  34762  brtxpsd3  34857  dfom5b  34873  dffun10  34875  bj-notalbii  35481  bj-ssbeq  35519  bj-ax12ssb  35524  bj-hbext  35577  bj-nfalt  35578  bj-substax12  35588  bj-nnfalt  35633  bj-nnfext  35634  ax11-pm2  35703  bj-sbnf  35708  bj-sblem  35712  eliminable-veqab  35734  eliminable-abeqv  35735  eliminable-abeqab  35736  bj-ralvw  35748  bj-sbeq  35770  bj-nfcf  35792  bj-snsetex  35833  bj-rcleqf  35895  bj-clex  35901  fvineqsneq  36282  wl-equsalvw  36396  wl-equsalcom  36400  wl-sb8et  36407  wl-2sb6d  36412  wl-alanbii  36423  wl-sb8eut  36431  poimirlem25  36502  poimirlem30  36507  heibor1lem  36666  sbcalfi  36973  mpobi123f  37019  mptbi12f  37023  ineccnvmo  37215  alrmomorn  37216  cocossss  37295  cossssid3  37328  cossssid4  37329  cosscnvssid4  37336  trcoss2  37343  dfeldisj4  37579  dfeldisj5  37580  disjres  37603  dvelimf-o  37788  axc11n-16  37797  pmapglbx  38629  sn-axrep5v  41030  dford4  41754  unielss  41953  onsupmaxb  41974  rp-fakeinunass  42252  rababg  42311  elmapintrab  42313  elinintrab  42314  undmrnresiss  42341  clss2lem  42348  cotrintab  42351  elintima  42390  relexp0eq  42438  dfhe3  42512  snhesn  42523  psshepw  42525  dffrege76  42676  frege77  42677  frege110  42710  dffrege115  42715  frege116  42716  frege118  42718  frege131  42731  ntrneikb  42831  ismnuprim  43039  rr-grothprimbi  43040  ismnushort  43046  rr-grothshortbi  43048  pm10.541  43112  pm10.542  43113  19.21vv  43121  19.31vv  43129  19.28vv  43131  pm11.62  43139  axc11next  43151  pm13.196a  43159  2sbc6g  43160  elnev  43183  hbexgVD  43653  rabssf  43794  2rexsb  45796  dfich2  46113  ichal  46121  spr0nelg  46131  mo0sn  47454  dffun3f  47681  setrec1lem2  47687  setrec2  47694  setis  47697  alimp-surprise  47781  alimp-no-surprise  47782