Theorem albii 1842

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

Syntax hints:   ↔ wb 209  ∀wal 1561

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

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  2albii  1843  3albii  1844  hbxfrbi  1848  alex  1849  2nalexn  1851  2exnaln  1852  imnang  1865  alexn  1868  19.26-2  1894  19.26-3an  1895  19.43OLD  1906  albiim  1912  2albiim  1913  empty  1929  19.32v  1963  19.31v  1964  19.23vv  1966  pm11.53v  1967  19.12vvv  2017  equsalvw  2027  2sb6  2122  sbrimvwOLD  2128  sbbiiev  2129  alrot3  2197  alrot4  2198  sbal  2206  sbalv  2207  19.21-2  2247  19.32  2271  19.31  2272  equsalv  2305  sbn  2317  sbrim  2341  aaan  2367  pm11.53  2380  19.12vv  2381  sb8v  2387  sb8f  2388  cbvsbvf  2397  equsal  2451  2sb6rf  2507  sbcom3  2540  sb8eulem  2628  eu1  2640  2mo2  2677  2eu1  2680  2eu1v  2681  2eu3  2683  euae  2689  nulmo  2742  eqabbw  2838  eqabcbw  2839  hblem  2896  hblemg  2897  eqabcb  2905  nfceqi  2924  eqabf  2956  ralbii2  3107  r2allem  3153  r3al  3203  r19.21t  3259  r19.23t  3261  ralcom4  3291  cbvralsvw  3316  sbralie  3343  sbralieOLD  3345  rabbi  3447  rabid2f  3448  rabid2im  3449  eqv  3467  eqvf  3468  abv  3469  abvALT  3470  ralv  3483  ceqsralt  3491  ceqsal  3494  ceqsalv  3496  rspc2gv  3594  ralxpxfr2d  3608  clel2g  3621  clel4g  3625  ralab  3659  ralrab2  3664  euind  3690  reu2  3691  reu3  3693  rmo4  3696  reu8  3699  rmo3f  3700  rmoim  3706  2reuswap  3712  2reuswap2  3713  reuind  3719  2reu5lem2  3722  2reu5lem3  3723  2rmoswap  3727  sbccomlem  3825  rmo2  3843  rmo3  3845  rmoanim  3850  dfss2  3925  ss2ab  4017  ss2rab  4025  rabss  4026  ss2rabd  4028  uniiunlem  4043  dfdif3OLD  4075  ssequn1  4141  unss  4145  ralunb  4152  ssin  4193  eq0f  4302  eq0  4305  eq0ALT  4306  ssdif0  4322  inssdif0  4330  ab0w  4335  ab0  4336  ab0ALT  4337  ab0orv  4339  disj  4407  disj3  4411  ssundif  4444  ralf0  4454  ralidmw  4473  ralidm  4474  pwss  4582  rabsssn  4630  rabeqsnd  4631  ralsnsg  4632  ralsng  4637  disjsn  4673  snssb  4744  pwpw0  4774  dfnfc2  4890  unissb  4902  elintrab  4921  ssintrab  4932  intun  4941  intprg  4942  dfiin2g  4991  iunssf  5003  iunssfOLD  5004  iunss  5005  iunssOLD  5006  dfdisj2  5074  cbvdisj  5082  cbvdisjv  5083  disjor  5087  dftr2  5214  dftr5  5216  axrep1  5233  axrep4v  5237  axrep4  5238  axrep5  5240  axrep6  5241  axrep6OLD  5242  zfrep6  5244  axsepgfromrep  5249  axnulALT  5259  vnexOLD  5273  inex1  5278  axpweq  5312  zfpow  5328  axpow2  5329  nfnid  5337  dtruALT  5350  reusv2lem4  5363  zfpair2  5396  prex  5400  elOLD  5411  ssextss  5425  moabexOLD  5431  dffr6  5608  dffr2  5613  dffr2ALT  5614  dfepfr  5636  frinxp  5735  ssrel2  5762  eqrelrel  5774  raliunxp  5816  relop  5827  dmopab3  5900  dm0rn0  5905  dm0rn0OLD  5906  reldm0  5909  rnopab3  5937  iresn0n0  6047  dffr3  6092  cotrg  6102  idrefALT  6104  asymref  6107  asymref2  6108  intirr  6109  dffr4  6311  sucel  6426  sb8iota  6492  dffun6  6536  dffun3  6537  dffun4  6538  dffun5  6539  dffun6f  6540  dffun7  6552  funopab  6560  funcnv2  6593  funcnv  6594  fun2cnv  6596  fun11  6599  fununi  6600  fnres  6652  mptfnf  6660  fnopabg  6662  tz6.12-2  6858  brprcneu  6861  brprcneuALT  6862  dffv2  6966  funcnvmpt  6981  fvn0ssdmfun  7059  dff13  7242  fnssintima  7350  eqoprab2bw  7470  eqoprab2b  7471  mpo2eqb  7532  ralrnmpo  7539  imaeqalov  7639  zfun  7723  uniex2  7725  funcnvuni  7917  ralxp3f  8121  frpoins3xpg  8124  frpoins3xp3g  8125  xpord3inddlem  8138  dfer2  8683  fiint  9274  marypha1lem  9381  marypha2lem3  9385  inf2  9580  axinf2  9597  ttrclss  9677  scottexs  9849  scott0s  9850  aceq1  10089  dfac4  10094  dfac7  10104  dfac0  10105  dfac1  10106  dfac10  10109  dfac10c  10110  dfac10b  10111  kmlem4  10125  kmlem12  10133  kmlem14  10135  kmlem15  10136  kmlem16  10137  dfackm  10138  ac6n  10457  axpowndlem3  10572  zfcndrep  10587  zfcndun  10588  zfcndpow  10589  axgroth5  10797  axgroth2  10798  axgroth4  10805  grothprim  10807  sstskm  10815  fimaxre3  12152  infm3  12165  nnwos  12930  cotr2g  15003  brtrclfv  15029  trclfvcotr  15036  rpnnen2lem12  16271  isprm2  16730  vdwmc2  17029  pgpfac1  20143  pgpfac  20147  ssdifidlprm  21446  iunocv  21791  2ndcdisj2  23575  hausdiag  23763  rnelfmlem  24070  alexsubALTlem3  24167  cnextfun  24182  itg2leub  25854  eqcuts2  27937  addsuniflem  28152  mulsuniflem  28300  onsfi  28507  mpteleeOLD  29154  nmoubi  31033  nmobndseqi  31040  nmobndseqiALT  31041  isch2  31484  isch3  31502  choc0  31587  nmopub  32169  nmfnleub  32186  xfree2  32706  mo5f  32745  nmo  32746  reuxfrdf  32747  rabsspr  32757  rabsstp  32758  inpr0  32788  cbvdisjf  32826  disjorf  32834  ssrelf  32872  funcnv5mpt  32924  ballotlem2  34796  bnj89  35027  bnj115  35031  bnj1143  35095  bnj110  35163  bnj611  35223  bnj864  35227  bnj865  35228  bnj1000  35246  bnj978  35254  bnj1049  35279  bnj1052  35280  bnj1090  35284  bnj1030  35292  bnj1133  35294  bnj1171  35305  bnj1172  35306  bnj1174  35308  bnj1176  35310  bnj1204  35317  bnj1253  35322  bnj1388  35338  bnj1523  35376  axnulALT2  35387  fineqvrep  35422  fineqvpow  35423  axreg  35435  axregscl  35436  axregs  35447  axpowg  35454  vonf1wev  35463  vonf1owevOLD  35465  axrepprim  36065  axunprim  36066  axpowprim  36067  axinfprim  36069  axacprim  36070  untuni  36072  dffr5  36117  elintfv  36128  dfon2lem8  36151  dfon2lem9  36152  19.12b  36162  brtxpsd3  36257  dfom5b  36273  dffun10  36275  disjeq1i  36565  ss-ax8  36598  cbvdisjvw2  36608  mh-setind  36909  regsfromregtco  36911  regsfromsetind  36912  regsfromunir1  36913  mh-prprimbi  36916  mh-unprimbi  36917  mh-infprim1bi  36919  mh-infprim2bi  36920  mh-infprim3bi  36921  bj-notalbii  37084  bj-cbvaew  37128  bj-ssbeq  37137  bj-ax12ssb  37142  bj-nfalt  37200  bj-substax12  37211  bj-nnfalt  37277  bj-nnfext  37278  ax11-pm2  37333  bj-sblem  37341  eliminable-veqab  37363  eliminable-abeqv  37364  eliminable-abeqab  37365  bj-ralvw  37376  bj-sbeq  37398  bj-nfcf  37420  bj-snsetex  37460  bj-rcleqf  37522  bj-clex  37528  bj-rep  37570  bj-axseprep  37571  fvineqsneq  37918  wl-equsalvw  38053  wl-equsalcom  38058  wl-sb9v  38064  wl-sb8eft  38066  wl-sb8et  38068  wl-2sb6d  38073  wl-alanbii  38084  wl-sb8eut  38093  wl-sb8eutv  38094  poimirlem25  38156  poimirlem30  38161  heibor1lem  38320  sbcalfi  38627  mpobi123f  38673  mptbi12f  38677  ineccnvmo  38868  alrmomorn  38869  ralmo  38871  ralrmo3  38875  cocossss  39037  cossssid3  39070  cossssid4  39071  cosscnvssid4  39078  trcoss2  39085  dfeldisj4  39323  dfeldisj5  39324  disjres  39355  dvelimf-o  39565  axc11n-16  39574  pmapglbx  40405  sn-axrep5v  42848  abbibw  43271  dford4  43618  unielss  43807  onsupmaxb  43828  rp-fakeinunass  44103  rababg  44162  elmapintrab  44164  elinintrab  44165  undmrnresiss  44192  clss2lem  44199  cotrintab  44202  elintima  44241  relexp0eq  44289  dfhe3  44363  snhesn  44374  psshepw  44376  dffrege76  44527  frege77  44528  frege110  44561  dffrege115  44566  frege116  44567  frege118  44569  frege131  44582  ntrneikb  44682  ismnuprim  44868  rr-grothprimbi  44869  ismnushort  44875  rr-grothshortbi  44877  pm10.541  44941  pm10.542  44942  19.21vv  44950  19.31vv  44958  19.28vv  44960  pm11.62  44968  axc11next  44980  pm13.196a  44988  2sbc6g  44989  elnev  45011  hbexgVD  45479  dfac5prim  45564  permaxext  45579  permaxrep  45580  permaxpow  45583  permac8prim  45588  rabssf  45695  sinnpoly  47483  2rexsb  47693  dfich2  48062  ichal  48070  spr0nelg  48080  mo0sn  49445  dffun3f  50311  setrec1lem2  50317  setrec2  50324  setis  50327  alimp-surprise  50409  alimp-no-surprise  50410