Theorem albii 1838

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

Syntax hints:   ↔ wb 208  ∀wal 1557

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

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  2albii  1839  3albii  1840  hbxfrbi  1844  alex  1845  2nalexn  1847  2exnaln  1848  imnang  1861  alexn  1864  19.26-2  1890  19.26-3an  1891  19.43OLD  1902  albiim  1908  2albiim  1909  empty  1925  19.32v  1959  19.31v  1960  19.23vv  1962  pm11.53v  1963  19.12vvv  2013  equsalvw  2023  2sb6  2118  sbrimvwOLD  2124  sbbiiev  2125  alrot3  2193  alrot4  2194  sbal  2202  sbalv  2203  19.21-2  2243  19.32  2267  19.31  2268  equsalv  2301  sbn  2313  sbrim  2337  aaan  2363  pm11.53  2376  19.12vv  2377  sb8v  2383  sb8f  2384  cbvsbvf  2393  equsal  2447  2sb6rf  2503  sbcom3  2536  sb8eulem  2624  eu1  2636  2mo2  2673  2eu1  2676  2eu1v  2677  2eu3  2679  euae  2685  nulmo  2738  eqabbw  2834  eqabcbw  2835  hblem  2892  hblemg  2893  eqabcb  2901  nfceqi  2920  eqabf  2952  ralbii2  3103  r2allem  3149  r3al  3199  r19.21t  3255  r19.23t  3257  ralcom4  3287  cbvralsvw  3312  sbralie  3339  sbralieOLD  3341  rabbi  3443  rabid2f  3444  rabid2im  3445  eqv  3463  eqvf  3464  abv  3465  abvALT  3466  ralv  3479  ceqsralt  3487  ceqsal  3490  ceqsalv  3492  rspc2gv  3591  ralxpxfr2d  3605  clel2g  3618  clel4g  3622  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  3822  rmo2  3840  rmo3  3842  rmoanim  3847  dfss2  3922  ss2ab  4014  ss2rab  4022  rabss  4023  ss2rabd  4025  uniiunlem  4040  dfdif3OLD  4072  ssequn1  4138  unss  4142  ralunb  4149  ssin  4190  eq0f  4299  eq0  4302  eq0ALT  4303  ssdif0  4318  inssdif0  4326  ab0w  4331  ab0  4332  ab0ALT  4333  ab0orv  4335  disj  4403  disj3  4407  ssundif  4440  ralf0  4450  ralidmw  4469  ralidm  4470  pwss  4578  rabsssn  4626  rabeqsnd  4627  ralsnsg  4628  ralsng  4633  disjsn  4669  snssb  4740  pwpw0  4770  dfnfc2  4886  unissb  4898  elintrab  4917  ssintrab  4928  intun  4937  intprg  4938  dfiin2g  4987  iunssf  4999  iunssfOLD  5000  iunss  5001  iunssOLD  5002  dfdisj2  5068  cbvdisj  5076  cbvdisjv  5077  disjor  5081  dftr2  5208  dftr5  5210  axrep1  5227  axrep4v  5231  axrep4  5232  axrep5  5234  axrep6  5235  axrep6OLD  5236  zfrep6  5238  axsepgfromrep  5243  axnulALT  5253  vnexOLD  5267  inex1  5272  axpweq  5306  zfpow  5322  axpow2  5323  nfnid  5331  dtruALT  5344  reusv2lem4  5357  zfpair2  5390  prex  5394  elOLD  5405  ssextss  5419  moabexOLD  5425  dffr6  5601  dffr2  5606  dffr2ALT  5607  dfepfr  5629  frinxp  5728  ssrel2  5755  eqrelrel  5767  raliunxp  5809  relop  5820  dmopab3  5893  dm0rn0  5898  dm0rn0OLD  5899  reldm0  5902  rnopab3  5930  iresn0n0  6038  dffr3  6083  cotrg  6093  idrefALT  6095  asymref  6098  asymref2  6099  intirr  6100  dffr4  6301  sucel  6416  sb8iota  6482  dffun6  6526  dffun3  6527  dffun4  6528  dffun5  6529  dffun6f  6530  dffun7  6542  funopab  6550  funcnv2  6583  funcnv  6584  fun2cnv  6586  fun11  6589  fununi  6590  fnres  6642  mptfnf  6650  fnopabg  6652  tz6.12-2  6848  brprcneu  6851  brprcneuALT  6852  dffv2  6956  funcnvmpt  6971  fvn0ssdmfun  7049  dff13  7232  fnssintima  7340  eqoprab2bw  7460  eqoprab2b  7461  mpo2eqb  7522  ralrnmpo  7529  imaeqalov  7629  zfun  7713  uniex2  7715  funcnvuni  7907  ralxp3f  8110  frpoins3xpg  8113  frpoins3xp3g  8114  xpord3inddlem  8127  dfer2  8672  fiint  9265  marypha1lem  9374  marypha2lem3  9378  inf2  9573  axinf2  9590  ttrclss  9670  scottexs  9840  scott0s  9841  aceq1  10068  dfac4  10073  dfac7  10084  dfac0  10085  dfac1  10086  dfac10  10089  dfac10c  10090  dfac10b  10091  kmlem4  10105  kmlem12  10113  kmlem14  10115  kmlem15  10116  kmlem16  10117  dfackm  10118  ac6n  10437  axpowndlem3  10552  zfcndrep  10567  zfcndun  10568  zfcndpow  10569  axgroth5  10777  axgroth2  10778  axgroth4  10785  grothprim  10787  sstskm  10795  fimaxre3  12133  infm3  12146  nnwos  12911  cotr2g  14984  brtrclfv  15010  trclfvcotr  15017  rpnnen2lem12  16238  isprm2  16697  vdwmc2  16996  pgpfac1  20103  pgpfac  20107  iunocv  21711  2ndcdisj2  23495  hausdiag  23683  rnelfmlem  23990  alexsubALTlem3  24087  cnextfun  24102  itg2leub  25774  eqcuts2  27854  addsuniflem  28069  mulsuniflem  28217  onsfi  28424  mpteleeOLD  29040  nmoubi  30919  nmobndseqi  30926  nmobndseqiALT  30927  isch2  31370  isch3  31388  choc0  31473  nmopub  32055  nmfnleub  32072  xfree2  32592  mo5f  32634  nmo  32635  reuxfrdf  32636  rabsspr  32647  rabsstp  32648  inpr0  32678  cbvdisjf  32718  disjorf  32726  ssrelf  32765  funcnv5mpt  32817  ssdifidlprm  33604  ballotlem2  34745  bnj89  34979  bnj115  34983  bnj1143  35047  bnj110  35115  bnj611  35175  bnj864  35179  bnj865  35180  bnj1000  35198  bnj978  35206  bnj1049  35231  bnj1052  35232  bnj1090  35236  bnj1030  35244  bnj1133  35246  bnj1171  35257  bnj1172  35258  bnj1174  35260  bnj1176  35262  bnj1204  35269  bnj1253  35274  bnj1388  35290  bnj1523  35328  axnulALT2  35339  fineqvrep  35370  fineqvpow  35371  axreg  35383  axregscl  35384  axregs  35395  axpowg  35402  vonf1owev  35411  axrepprim  36005  axunprim  36006  axpowprim  36007  axinfprim  36009  axacprim  36010  untuni  36012  dffr5  36057  elintfv  36068  dfon2lem8  36091  dfon2lem9  36092  19.12b  36102  brtxpsd3  36197  dfom5b  36213  dffun10  36215  disjeq1i  36505  ss-ax8  36538  cbvdisjvw2  36548  mh-setind  36849  regsfromregtco  36851  regsfromsetind  36852  regsfromunir1  36853  mh-prprimbi  36856  mh-unprimbi  36857  mh-infprim1bi  36859  mh-infprim2bi  36860  mh-infprim3bi  36861  bj-notalbii  37025  bj-cbvaew  37069  bj-ssbeq  37078  bj-ax12ssb  37083  bj-nfalt  37141  bj-substax12  37152  bj-nnfalt  37218  bj-nnfext  37219  ax11-pm2  37274  bj-sblem  37282  eliminable-veqab  37304  eliminable-abeqv  37305  eliminable-abeqab  37306  bj-ralvw  37317  bj-sbeq  37339  bj-nfcf  37361  bj-snsetex  37401  bj-rcleqf  37463  bj-clex  37469  bj-rep  37511  bj-axseprep  37512  fvineqsneq  37859  wl-equsalvw  37994  wl-equsalcom  37999  wl-sb9v  38005  wl-sb8eft  38007  wl-sb8et  38009  wl-2sb6d  38014  wl-alanbii  38025  wl-sb8eut  38034  wl-sb8eutv  38035  poimirlem25  38097  poimirlem30  38102  heibor1lem  38261  sbcalfi  38568  mpobi123f  38614  mptbi12f  38618  ineccnvmo  38809  alrmomorn  38810  ralmo  38812  ralrmo3  38816  cocossss  38978  cossssid3  39011  cossssid4  39012  cosscnvssid4  39019  trcoss2  39026  dfeldisj4  39264  dfeldisj5  39265  disjres  39296  dvelimf-o  39506  axc11n-16  39515  pmapglbx  40346  sn-axrep5v  42789  abbibw  43212  dford4  43559  unielss  43748  onsupmaxb  43769  rp-fakeinunass  44044  rababg  44103  elmapintrab  44105  elinintrab  44106  undmrnresiss  44133  clss2lem  44140  cotrintab  44143  elintima  44182  relexp0eq  44230  dfhe3  44304  snhesn  44315  psshepw  44317  dffrege76  44468  frege77  44469  frege110  44502  dffrege115  44507  frege116  44508  frege118  44510  frege131  44523  ntrneikb  44623  ismnuprim  44823  rr-grothprimbi  44824  ismnushort  44830  rr-grothshortbi  44832  pm10.541  44896  pm10.542  44897  19.21vv  44905  19.31vv  44913  19.28vv  44915  pm11.62  44923  axc11next  44935  pm13.196a  44943  2sbc6g  44944  elnev  44966  hbexgVD  45434  dfac5prim  45519  permaxext  45534  permaxrep  45535  permaxpow  45538  permac8prim  45543  rabssf  45650  sinnpoly  47438  2rexsb  47648  dfich2  48017  ichal  48025  spr0nelg  48035  mo0sn  49390  dffun3f  50256  setrec1lem2  50262  setrec2  50269  setis  50272  alimp-surprise  50354  alimp-no-surprise  50355