Theorem albii 1826

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

Syntax hints:   ↔ wb 207  ∀wal 1545

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

This theorem depends on definitions:  df-bi 208

This theorem is referenced by:  2albii  1827  3albii  1828  hbxfrbi  1832  alex  1833  2nalexn  1835  2exnaln  1836  imnang  1849  alexn  1852  19.26-2  1878  19.26-3an  1879  19.43OLD  1890  albiim  1896  2albiim  1897  empty  1913  19.32v  1947  19.31v  1948  19.23vv  1950  pm11.53v  1951  19.12vvv  2001  equsalvw  2011  2sb6  2097  sbrimvw  2102  sbbiiev  2103  alrot3  2171  alrot4  2172  sbal  2180  sbalv  2181  19.21-2  2221  19.32  2245  19.31  2246  equsalv  2279  sbn  2291  sbrim  2315  aaan  2341  pm11.53  2354  19.12vv  2355  sb8v  2361  sb8f  2362  cbvsbvf  2371  equsal  2425  2sb6rf  2481  sbcom3  2514  sb8eulem  2602  eu1  2614  2mo2  2651  2eu1  2655  2eu1v  2656  2eu3  2658  euae  2664  nulmo  2717  eqabbw  2813  eqabcbw  2814  hblem  2871  hblemg  2872  eqabcb  2880  nfceqi  2899  eqabf  2931  ralbii2  3082  r2allem  3128  r3al  3178  r19.21t  3234  r19.23t  3236  ralcom4  3266  cbvralsvw  3291  sbralie  3318  sbralieOLD  3320  rabbi  3422  rabid2f  3423  rabid2im  3424  eqv  3442  eqvf  3443  abv  3444  abvALT  3445  ralv  3459  ceqsralt  3467  ceqsal  3470  ceqsalv  3472  rspc2gv  3577  ralxpxfr2d  3591  clel2g  3604  clel4g  3608  ralab  3641  ralrab2  3646  euind  3672  reu2  3673  reu3  3675  rmo4  3678  reu8  3681  rmo3f  3682  rmoim  3688  2reuswap  3694  2reuswap2  3695  reuind  3701  2reu5lem2  3704  2reu5lem3  3705  2rmoswap  3709  sbccomlem  3808  rmo2  3826  rmo3  3828  rmoanim  3833  dfss2  3908  ss2ab  3999  ss2rab  4007  rabss  4008  ss2rabd  4010  uniiunlem  4025  dfdif3OLD  4056  ssequn1  4122  unss  4126  ralunb  4133  ssin  4174  eq0f  4282  eq0  4285  eq0ALT  4286  ssdif0  4301  inssdif0  4309  ab0w  4314  ab0  4315  ab0ALT  4316  ab0orv  4318  disj  4385  disj3  4389  ssundif  4422  ralf0  4432  ralidmw  4451  ralidm  4452  pwss  4559  rabsssn  4607  rabeqsnd  4608  ralsnsg  4609  ralsng  4614  disjsn  4650  snssb  4721  pwpw0  4751  dfnfc2  4867  unissb  4878  elintrab  4897  ssintrab  4908  intun  4917  intprg  4918  dfiin2g  4967  iunssf  4979  iunssfOLD  4980  iunss  4981  iunssOLD  4982  dfdisj2  5048  cbvdisj  5056  cbvdisjv  5057  disjor  5061  dftr2  5188  dftr5  5190  axrep1  5207  axrep4v  5211  axrep4  5212  axrep5  5214  axrep6  5215  axrep6OLD  5216  zfrep6  5218  axsepgfromrep  5223  axnulALT  5233  vnexOLD  5247  inex1  5252  axpweq  5286  zfpow  5302  axpow2  5303  nfnid  5311  dtruALT  5324  reusv2lem4  5337  zfpair2  5370  prex  5374  elOLD  5385  ssextss  5399  moabexOLD  5405  dffr6  5581  dffr2  5586  dffr2ALT  5587  dfepfr  5609  frinxp  5708  ssrel2  5735  eqrelrel  5747  raliunxp  5788  relop  5799  dmopab3  5868  dm0rn0  5873  dm0rn0OLD  5874  reldm0  5877  rnopab3  5905  iresn0n0  6013  dffr3  6058  cotrg  6068  idrefALT  6070  asymref  6073  asymref2  6074  intirr  6075  dffr4  6278  sucel  6393  sb8iota  6459  dffun6  6503  dffun3  6504  dffun4  6505  dffun5  6506  dffun6f  6507  dffun7  6519  funopab  6527  funcnv2  6560  funcnv  6561  fun2cnv  6563  fun11  6566  fununi  6567  fnres  6619  mptfnf  6627  fnopabg  6629  tz6.12-2  6821  brprcneu  6824  brprcneuALT  6825  dffv2  6929  funcnvmpt  6944  fvn0ssdmfun  7022  dff13  7205  fnssintima  7313  eqoprab2bw  7433  eqoprab2b  7434  mpo2eqb  7495  ralrnmpo  7502  imaeqalov  7602  zfun  7686  uniex2  7688  funcnvuni  7879  ralxp3f  8084  frpoins3xpg  8087  frpoins3xp3g  8088  xpord3inddlem  8101  dfer2  8641  fiint  9234  marypha1lem  9343  marypha2lem3  9347  inf2  9542  axinf2  9559  ttrclss  9639  scottexs  9809  scott0s  9810  aceq1  10037  dfac4  10042  dfac7  10053  dfac0  10054  dfac1  10055  dfac10  10058  dfac10c  10059  dfac10b  10060  kmlem4  10074  kmlem12  10082  kmlem14  10084  kmlem15  10085  kmlem16  10086  dfackm  10087  ac6n  10405  axpowndlem3  10520  zfcndrep  10535  zfcndun  10536  zfcndpow  10537  axgroth5  10745  axgroth2  10746  axgroth4  10753  grothprim  10755  sstskm  10763  fimaxre3  12100  infm3  12113  nnwos  12863  cotr2g  14936  brtrclfv  14962  trclfvcotr  14969  rpnnen2lem12  16190  isprm2  16649  vdwmc2  16948  pgpfac1  20055  pgpfac  20059  iunocv  21663  2ndcdisj2  23447  hausdiag  23635  rnelfmlem  23942  alexsubALTlem3  24039  cnextfun  24054  itg2leub  25726  eqcuts2  27803  addsuniflem  28018  mulsuniflem  28166  onsfi  28373  mpteleeOLD  28989  nmoubi  30868  nmobndseqi  30875  nmobndseqiALT  30876  isch2  31319  isch3  31337  choc0  31422  nmopub  32004  nmfnleub  32021  xfree2  32541  mo5f  32583  nmo  32584  reuxfrdf  32585  rabsspr  32596  rabsstp  32597  inpr0  32627  cbvdisjf  32667  disjorf  32675  ssrelf  32714  funcnv5mpt  32766  ssdifidlprm  33548  ballotlem2  34680  bnj89  34911  bnj115  34915  bnj1143  34979  bnj110  35047  bnj611  35107  bnj864  35111  bnj865  35112  bnj1000  35130  bnj978  35138  bnj1049  35163  bnj1052  35164  bnj1090  35168  bnj1030  35176  bnj1133  35178  bnj1171  35189  bnj1172  35190  bnj1174  35192  bnj1176  35194  bnj1204  35201  bnj1253  35206  bnj1388  35222  bnj1523  35260  axnulALT2  35271  fineqvrep  35302  fineqvpow  35303  axreg  35315  axregscl  35316  axregs  35327  axpowg  35334  vonf1owev  35343  axrepprim  35937  axunprim  35938  axpowprim  35939  axinfprim  35941  axacprim  35942  untuni  35944  dffr5  35989  elintfv  36000  dfon2lem8  36023  dfon2lem9  36024  19.12b  36034  brtxpsd3  36129  dfom5b  36145  dffun10  36147  disjeq1i  36427  ss-ax8  36460  cbvdisjvw2  36470  mh-setind  36771  regsfromregtco  36773  regsfromsetind  36774  regsfromunir1  36775  mh-prprimbi  36778  mh-unprimbi  36779  mh-infprim1bi  36781  mh-infprim2bi  36782  mh-infprim3bi  36783  bj-notalbii  36947  bj-cbvaew  36991  bj-ssbeq  37000  bj-ax12ssb  37005  bj-nfalt  37063  bj-substax12  37074  bj-nnfalt  37140  bj-nnfext  37141  ax11-pm2  37196  bj-sblem  37204  eliminable-veqab  37226  eliminable-abeqv  37227  eliminable-abeqab  37228  bj-ralvw  37239  bj-sbeq  37261  bj-nfcf  37283  bj-snsetex  37323  bj-rcleqf  37385  bj-clex  37391  bj-rep  37433  bj-axseprep  37434  fvineqsneq  37781  wl-equsalvw  37916  wl-equsalcom  37921  wl-sb9v  37927  wl-sb8eft  37929  wl-sb8et  37931  wl-2sb6d  37936  wl-alanbii  37947  wl-sb8eut  37956  wl-sb8eutv  37957  poimirlem25  38019  poimirlem30  38024  heibor1lem  38183  sbcalfi  38490  mpobi123f  38536  mptbi12f  38540  ineccnvmo  38731  alrmomorn  38732  ralmo  38734  ralrmo3  38738  cocossss  38900  cossssid3  38933  cossssid4  38934  cosscnvssid4  38941  trcoss2  38948  dfeldisj4  39186  dfeldisj5  39187  disjres  39218  dvelimf-o  39428  axc11n-16  39437  pmapglbx  40268  sn-axrep5v  42711  abbibw  43134  dford4  43481  unielss  43670  onsupmaxb  43691  rp-fakeinunass  43966  rababg  44025  elmapintrab  44027  elinintrab  44028  undmrnresiss  44055  clss2lem  44062  cotrintab  44065  elintima  44104  relexp0eq  44152  dfhe3  44226  snhesn  44237  psshepw  44239  dffrege76  44390  frege77  44391  frege110  44424  dffrege115  44429  frege116  44430  frege118  44432  frege131  44445  ntrneikb  44545  ismnuprim  44745  rr-grothprimbi  44746  ismnushort  44752  rr-grothshortbi  44754  pm10.541  44818  pm10.542  44819  19.21vv  44827  19.31vv  44835  19.28vv  44837  pm11.62  44845  axc11next  44857  pm13.196a  44865  2sbc6g  44866  elnev  44888  hbexgVD  45356  dfac5prim  45441  permaxext  45456  permaxrep  45457  permaxpow  45460  permac8prim  45465  rabssf  45573  sinnpoly  47361  2rexsb  47571  dfich2  47940  ichal  47948  spr0nelg  47958  mo0sn  49313  dffun3f  50179  setrec1lem2  50185  setrec2  50192  setis  50195  alimp-surprise  50277  alimp-no-surprise  50278