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  6040  dffr3  6085  cotrg  6095  idrefALT  6097  asymref  6100  asymref2  6101  intirr  6102  dffr4  6303  sucel  6418  sb8iota  6484  dffun6  6528  dffun3  6529  dffun4  6530  dffun5  6531  dffun6f  6532  dffun7  6544  funopab  6552  funcnv2  6585  funcnv  6586  fun2cnv  6588  fun11  6591  fununi  6592  fnres  6644  mptfnf  6652  fnopabg  6654  tz6.12-2  6850  brprcneu  6853  brprcneuALT  6854  dffv2  6958  funcnvmpt  6973  fvn0ssdmfun  7051  dff13  7234  fnssintima  7342  eqoprab2bw  7462  eqoprab2b  7463  mpo2eqb  7524  ralrnmpo  7531  imaeqalov  7631  zfun  7715  uniex2  7717  funcnvuni  7909  ralxp3f  8112  frpoins3xpg  8115  frpoins3xp3g  8116  xpord3inddlem  8129  dfer2  8674  fiint  9267  marypha1lem  9376  marypha2lem3  9380  inf2  9575  axinf2  9592  ttrclss  9672  scottexs  9842  scott0s  9843  aceq1  10070  dfac4  10075  dfac7  10086  dfac0  10087  dfac1  10088  dfac10  10091  dfac10c  10092  dfac10b  10093  kmlem4  10107  kmlem12  10115  kmlem14  10117  kmlem15  10118  kmlem16  10119  dfackm  10120  ac6n  10439  axpowndlem3  10554  zfcndrep  10569  zfcndun  10570  zfcndpow  10571  axgroth5  10779  axgroth2  10780  axgroth4  10787  grothprim  10789  sstskm  10797  fimaxre3  12135  infm3  12148  nnwos  12913  cotr2g  14986  brtrclfv  15012  trclfvcotr  15019  rpnnen2lem12  16240  isprm2  16699  vdwmc2  16998  pgpfac1  20105  pgpfac  20109  iunocv  21713  2ndcdisj2  23497  hausdiag  23685  rnelfmlem  23992  alexsubALTlem3  24089  cnextfun  24104  itg2leub  25776  eqcuts2  27856  addsuniflem  28071  mulsuniflem  28219  onsfi  28426  mpteleeOLD  29042  nmoubi  30921  nmobndseqi  30928  nmobndseqiALT  30929  isch2  31372  isch3  31390  choc0  31475  nmopub  32057  nmfnleub  32074  xfree2  32594  mo5f  32636  nmo  32637  reuxfrdf  32638  rabsspr  32649  rabsstp  32650  inpr0  32680  cbvdisjf  32720  disjorf  32728  ssrelf  32767  funcnv5mpt  32819  ssdifidlprm  33606  ballotlem2  34747  bnj89  34981  bnj115  34985  bnj1143  35049  bnj110  35117  bnj611  35177  bnj864  35181  bnj865  35182  bnj1000  35200  bnj978  35208  bnj1049  35233  bnj1052  35234  bnj1090  35238  bnj1030  35246  bnj1133  35248  bnj1171  35259  bnj1172  35260  bnj1174  35262  bnj1176  35264  bnj1204  35271  bnj1253  35276  bnj1388  35292  bnj1523  35330  axnulALT2  35341  fineqvrep  35374  fineqvpow  35375  axreg  35387  axregscl  35388  axregs  35399  axpowg  35406  vonf1wev  35415  vonf1owevOLD  35417  axrepprim  36016  axunprim  36017  axpowprim  36018  axinfprim  36020  axacprim  36021  untuni  36023  dffr5  36068  elintfv  36079  dfon2lem8  36102  dfon2lem9  36103  19.12b  36113  brtxpsd3  36208  dfom5b  36224  dffun10  36226  disjeq1i  36516  ss-ax8  36549  cbvdisjvw2  36559  mh-setind  36860  regsfromregtco  36862  regsfromsetind  36863  regsfromunir1  36864  mh-prprimbi  36867  mh-unprimbi  36868  mh-infprim1bi  36870  mh-infprim2bi  36871  mh-infprim3bi  36872  bj-notalbii  37036  bj-cbvaew  37080  bj-ssbeq  37089  bj-ax12ssb  37094  bj-nfalt  37152  bj-substax12  37163  bj-nnfalt  37229  bj-nnfext  37230  ax11-pm2  37285  bj-sblem  37293  eliminable-veqab  37315  eliminable-abeqv  37316  eliminable-abeqab  37317  bj-ralvw  37328  bj-sbeq  37350  bj-nfcf  37372  bj-snsetex  37412  bj-rcleqf  37474  bj-clex  37480  bj-rep  37522  bj-axseprep  37523  fvineqsneq  37870  wl-equsalvw  38005  wl-equsalcom  38010  wl-sb9v  38016  wl-sb8eft  38018  wl-sb8et  38020  wl-2sb6d  38025  wl-alanbii  38036  wl-sb8eut  38045  wl-sb8eutv  38046  poimirlem25  38108  poimirlem30  38113  heibor1lem  38272  sbcalfi  38579  mpobi123f  38625  mptbi12f  38629  ineccnvmo  38820  alrmomorn  38821  ralmo  38823  ralrmo3  38827  cocossss  38989  cossssid3  39022  cossssid4  39023  cosscnvssid4  39030  trcoss2  39037  dfeldisj4  39275  dfeldisj5  39276  disjres  39307  dvelimf-o  39517  axc11n-16  39526  pmapglbx  40357  sn-axrep5v  42800  abbibw  43223  dford4  43570  unielss  43759  onsupmaxb  43780  rp-fakeinunass  44055  rababg  44114  elmapintrab  44116  elinintrab  44117  undmrnresiss  44144  clss2lem  44151  cotrintab  44154  elintima  44193  relexp0eq  44241  dfhe3  44315  snhesn  44326  psshepw  44328  dffrege76  44479  frege77  44480  frege110  44513  dffrege115  44518  frege116  44519  frege118  44521  frege131  44534  ntrneikb  44634  ismnuprim  44834  rr-grothprimbi  44835  ismnushort  44841  rr-grothshortbi  44843  pm10.541  44907  pm10.542  44908  19.21vv  44916  19.31vv  44924  19.28vv  44926  pm11.62  44934  axc11next  44946  pm13.196a  44954  2sbc6g  44955  elnev  44977  hbexgVD  45445  dfac5prim  45530  permaxext  45545  permaxrep  45546  permaxpow  45549  permac8prim  45554  rabssf  45661  sinnpoly  47449  2rexsb  47659  dfich2  48028  ichal  48036  spr0nelg  48046  mo0sn  49401  dffun3f  50267  setrec1lem2  50273  setrec2  50280  setis  50283  alimp-surprise  50365  alimp-no-surprise  50366