Theorem albii 1820

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

Syntax hints:   ↔ wb 206  ∀wal 1539

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  2albii  1821  3albii  1822  hbxfrbi  1826  alex  1827  2nalexn  1829  2exnaln  1830  imnang  1843  alexn  1846  19.26-2  1872  19.26-3an  1873  19.43OLD  1884  albiim  1890  2albiim  1891  empty  1907  19.32v  1941  19.31v  1942  19.23vv  1944  pm11.53v  1945  19.12vvv  1995  equsalvw  2005  2sb6  2091  sbrimvw  2096  sbbiiev  2097  alrot3  2165  alrot4  2166  sbal  2174  sbalv  2175  19.21-2  2214  19.32  2238  19.31  2239  equsalv  2272  sbn  2284  sbrim  2308  sbnfOLD  2316  aaan  2335  pm11.53  2348  19.12vv  2349  sb8v  2355  sb8f  2356  cbvsbvf  2365  equsal  2419  2sb6rf  2475  sbcom3  2508  sb8eulem  2595  eu1  2607  2mo2  2644  2eu1  2648  2eu1v  2649  2eu3  2651  euae  2657  nulmo  2710  eqabbw  2806  eqabcbw  2807  hblem  2864  hblemg  2865  eqabcb  2873  nfceqi  2892  eqabf  2925  ralbii2  3075  r2allem  3121  r3al  3171  r19.21t  3227  r19.23t  3229  ralcom4  3259  cbvralsvw  3284  sbralie  3319  sbralieOLD  3321  rabbi  3426  rabid2f  3427  rabid2im  3428  eqv  3447  eqvf  3448  abv  3449  abvALT  3450  ralv  3464  ceqsralt  3472  ceqsal  3475  ceqsalv  3477  rspc2gv  3583  ralxpxfr2d  3597  clel2g  3610  clel4g  3614  elabgtOLDOLD  3625  ralab  3648  ralrab2  3653  euind  3679  reu2  3680  reu3  3682  rmo4  3685  reu8  3688  rmo3f  3689  rmoim  3695  2reuswap  3701  2reuswap2  3702  reuind  3708  2reu5lem2  3711  2reu5lem3  3712  2rmoswap  3716  sbccomlem  3816  rmo2  3834  rmo3  3836  rmoanim  3841  dfss2  3916  ss2abim  4009  ss2ab  4010  ss2rab  4018  rabss  4019  ss2rabd  4021  uniiunlem  4036  dfdif3OLD  4067  ssequn1  4135  unss  4139  ralunb  4146  ssin  4188  eq0f  4296  eq0  4299  eq0ALT  4300  ssdif0  4315  inssdif0  4323  ab0w  4328  ab0  4329  ab0ALT  4330  ab0orv  4332  eq0rdv  4356  disj  4399  disj3  4403  ssundif  4437  ralidmw  4457  ralidm  4461  ralf0  4463  pwss  4572  rabsssn  4620  rabeqsnd  4621  ralsnsg  4622  ralsng  4627  disjsn  4663  snssb  4734  pwpw0  4764  dfnfc2  4880  unissb  4891  elintrab  4910  ssintrab  4921  intun  4930  intprg  4931  dfiin2g  4981  iunssf  4993  iunssfOLD  4994  iunss  4995  iunssOLD  4996  dfdisj2  5062  cbvdisj  5070  cbvdisjv  5071  disjor  5075  dftr2  5202  dftr5  5204  axrep1  5220  axrep4v  5224  axrep4  5225  axrep5  5227  axrep6  5228  axrep6OLD  5229  axsepgfromrep  5234  axnulALT  5244  vnex  5254  inex1  5257  axpweq  5291  zfpow  5306  axpow2  5307  nfnid  5315  dtruALT  5328  reusv2lem4  5341  zfpair2  5373  el  5382  ssextss  5396  moabexOLD  5402  dffr6  5575  dffr2  5580  dffr2ALT  5581  dfepfr  5603  frinxp  5702  ssrel2  5729  eqrelrel  5741  raliunxp  5783  relop  5794  dmopab3  5863  dm0rn0  5868  dm0rn0OLD  5869  reldm0  5872  rnopab3  5900  iresn0n0  6007  dffr3  6052  cotrg  6062  idrefALT  6064  asymref  6067  asymref2  6068  intirr  6069  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  tz6.12-2  6815  brprcneu  6818  brprcneuALT  6819  dffv2  6923  fvn0ssdmfun  7013  dff13  7194  fnssintima  7302  eqoprab2bw  7422  eqoprab2b  7423  mpo2eqb  7484  ralrnmpo  7491  imaeqalov  7591  zfun  7675  uniex2  7677  funcnvuni  7868  ralxp3f  8073  frpoins3xpg  8076  frpoins3xp3g  8077  xpord3inddlem  8090  dfer2  8629  fiint  9218  marypha1lem  9324  marypha2lem3  9328  inf2  9520  axinf2  9537  ttrclss  9617  scottexs  9787  scott0s  9788  aceq1  10015  dfac4  10020  dfac7  10031  dfac0  10032  dfac1  10033  dfac10  10036  dfac10c  10037  dfac10b  10038  kmlem4  10052  kmlem12  10060  kmlem14  10062  kmlem15  10063  kmlem16  10064  dfackm  10065  ac6n  10383  axpowndlem3  10497  zfcndrep  10512  zfcndun  10513  zfcndpow  10514  axgroth5  10722  axgroth2  10723  axgroth4  10730  grothprim  10732  sstskm  10740  fimaxre3  12075  infm3  12088  nnwos  12815  cotr2g  14885  brtrclfv  14911  trclfvcotr  14918  rpnnen2lem12  16136  isprm2  16595  vdwmc2  16893  pgpfac1  19996  pgpfac  20000  iunocv  21620  2ndcdisj2  23373  hausdiag  23561  rnelfmlem  23868  alexsubALTlem3  23965  cnextfun  23980  itg2leub  25663  eqscut2  27748  addsuniflem  27945  mulsuniflem  28089  onsfi  28284  mpteleeOLD  28875  nmoubi  30754  nmobndseqi  30761  nmobndseqiALT  30762  isch2  31205  isch3  31223  choc0  31308  nmopub  31890  nmfnleub  31907  xfree2  32427  mo5f  32470  nmo  32471  reuxfrdf  32472  rabsspr  32483  rabsstp  32484  inpr0  32514  cbvdisjf  32553  disjorf  32561  ssrelf  32600  funcnvmpt  32651  funcnv5mpt  32652  ssdifidlprm  33430  ballotlem2  34523  bnj89  34754  bnj115  34758  bnj1143  34823  bnj110  34891  bnj611  34951  bnj864  34955  bnj865  34956  bnj1000  34974  bnj978  34982  bnj1049  35007  bnj1052  35008  bnj1090  35012  bnj1030  35020  bnj1133  35022  bnj1171  35033  bnj1172  35034  bnj1174  35036  bnj1176  35038  bnj1204  35045  bnj1253  35050  bnj1388  35066  bnj1523  35104  axreg  35146  axregscl  35147  fineqvrep  35158  fineqvpow  35159  axregs  35166  vonf1owev  35173  axrepprim  35767  axunprim  35768  axpowprim  35769  axinfprim  35771  axacprim  35772  untuni  35774  dffr5  35819  elintfv  35830  dfon2lem8  35853  dfon2lem9  35854  19.12b  35864  brtxpsd3  35959  dfom5b  35975  dffun10  35977  disjeq1i  36257  ss-ax8  36290  cbvdisjvw2  36300  bj-notalbii  36679  bj-ssbeq  36718  bj-ax12ssb  36723  bj-hbext  36775  bj-nfalt  36776  bj-substax12  36786  bj-nnfalt  36831  bj-nnfext  36832  ax11-pm2  36901  bj-sblem  36909  eliminable-veqab  36931  eliminable-abeqv  36932  eliminable-abeqab  36933  bj-ralvw  36944  bj-sbeq  36966  bj-nfcf  36988  bj-snsetex  37028  bj-rcleqf  37090  bj-clex  37096  fvineqsneq  37477  wl-equsalvw  37603  wl-equsalcom  37608  wl-sb9v  37614  wl-sb8eft  37616  wl-sb8et  37618  wl-2sb6d  37623  wl-alanbii  37634  wl-sb8eut  37643  wl-sb8eutv  37644  poimirlem25  37706  poimirlem30  37711  heibor1lem  37870  sbcalfi  38177  mpobi123f  38223  mptbi12f  38227  ineccnvmo  38410  alrmomorn  38411  cocossss  38559  cossssid3  38592  cossssid4  38593  cosscnvssid4  38600  trcoss2  38607  dfeldisj4  38839  dfeldisj5  38840  disjres  38863  dvelimf-o  39049  axc11n-16  39058  pmapglbx  39889  sn-axrep5v  42335  abbibw  42796  dford4  43147  unielss  43336  onsupmaxb  43357  rp-fakeinunass  43633  rababg  43692  elmapintrab  43694  elinintrab  43695  undmrnresiss  43722  clss2lem  43729  cotrintab  43732  elintima  43771  relexp0eq  43819  dfhe3  43893  snhesn  43904  psshepw  43906  dffrege76  44057  frege77  44058  frege110  44091  dffrege115  44096  frege116  44097  frege118  44099  frege131  44112  ntrneikb  44212  ismnuprim  44412  rr-grothprimbi  44413  ismnushort  44419  rr-grothshortbi  44421  pm10.541  44485  pm10.542  44486  19.21vv  44494  19.31vv  44502  19.28vv  44504  pm11.62  44512  axc11next  44524  pm13.196a  44532  2sbc6g  44533  elnev  44555  hbexgVD  45023  dfac5prim  45108  permaxext  45123  permaxrep  45124  permaxpow  45127  permac8prim  45132  rabssf  45241  sinnpoly  47016  2rexsb  47226  dfich2  47583  ichal  47591  spr0nelg  47601  mo0sn  48941  dffun3f  49808  setrec1lem2  49814  setrec2  49821  setis  49824  alimp-surprise  49906  alimp-no-surprise  49907