Theorem albii 1827

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

Syntax hints:   ↔ wb 209  ∀wal 1541

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

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  2albii  1828  hbxfrbi  1832  alex  1833  2nalexn  1835  2exnaln  1836  imnang  1849  alexn  1852  nfnbiOLD  1863  19.26-2  1879  19.26-3an  1880  19.43OLD  1891  albiim  1897  2albiim  1898  empty  1914  19.32v  1948  19.31v  1949  19.23vv  1951  pm11.53v  1952  19.12vvv  1997  equsalvw  2012  2sb6  2092  sbrimvlem  2097  sbcom3vv  2102  alrot3  2161  alrot4  2162  sbal  2163  sbalv  2164  19.21-2  2207  19.32  2231  19.31  2232  equsalv  2264  sbn  2281  aaan  2333  pm11.53  2347  19.12vv  2348  sbievg  2362  equsal  2416  2sb6rf  2472  sbcom3  2509  sb8eulem  2597  eu1  2611  2mo2  2648  2eu1  2651  2eu1v  2652  2eu3  2654  euae  2660  nulmo  2713  abeq2w  2815  hblem  2867  hblemg  2868  abeq2  2869  abeq1  2870  abbiOLD  2877  nfcriOLD  2894  nfcriOLDOLD  2895  nfcriiOLD  2897  nfceqi  2901  abeq2f  2937  ralbii2  3086  r19.21v  3098  r2allem  3121  r3al  3123  r19.21t  3135  nfra2w  3149  ralcom4  3157  r19.23t  3232  rabid2  3293  rabid2f  3294  rabbi  3295  moel  3335  eqv  3417  eqvf  3418  abv  3419  abvALT  3420  ralv  3432  ceqsralt  3439  ceqsalv  3443  rspc2gv  3546  ralxpxfr2d  3553  clel2g  3566  clel4g  3571  elabgt  3581  elabg  3585  ralab  3606  ralrab2  3612  euind  3637  reu2  3638  reu3  3640  rmo4  3643  reu8  3646  rmo3f  3647  rmoim  3653  2reuswap  3659  2reuswap2  3660  reuind  3666  2reu5lem2  3669  2reu5lem3  3670  2rmoswap  3674  rmo2  3799  rmo3  3801  rmoanim  3806  dfss2  3886  dfss2OLD  3887  ss2ab  3973  ss2rab  3984  rabss  3985  uniiunlem  3999  dfdif3  4029  ssequn1  4094  unss  4098  ralunb  4105  ssin  4145  vn0  4253  eq0f  4255  eq0  4258  eq0ALT  4259  ssdif0  4278  inssdif0  4284  ab0w  4288  ab0  4289  ab0OLD  4290  ab0ALT  4291  ab0orv  4293  eq0rdv  4319  disj  4362  disjOLD  4363  disj3  4368  ssundif  4399  ralidmw  4419  ralidm  4423  ralf0  4425  ralf0OLD  4429  pwss  4538  rabsssn  4583  ralsnsg  4584  ralsng  4589  disjsn  4627  snssg  4698  pwpw0  4726  pwsnOLD  4812  dfnfc2  4843  unissb  4853  elintrab  4871  ssintrab  4882  intun  4891  intprg  4892  intprOLD  4894  dfiin2g  4941  iunssf  4953  iunss  4954  dfdisj2  5020  cbvdisj  5028  disjor  5033  dftr2  5163  dftr5  5164  axrep1  5180  axrep5  5185  axrep6  5186  axsepgfromrep  5190  axnulALT  5197  vnex  5207  inex1  5210  axpweq  5257  zfpow  5259  axpow2  5260  axpow3  5261  nfnid  5268  dtruALT  5281  reusv2lem4  5294  zfpair2  5323  dtruALT2  5328  ssextss  5338  moabex  5343  dffr2  5515  dffr2ALT  5516  dfepfr  5536  frinxp  5631  ssrel2  5656  eqrelrel  5667  reliun  5686  raliunxp  5708  relop  5719  dmopab3  5788  dm0rn0  5794  reldm0  5797  iresn0n0  5923  dffr3  5967  cotrg  5976  idrefALT  5978  asymref  5981  asymref2  5982  intirr  5983  dffr4  6178  sucel  6286  sb8iota  6350  dffun2  6390  dffun3  6391  dffun4  6392  dffun5  6393  dffun6f  6394  dffun7  6407  funopab  6415  funcnv2  6448  funcnv  6449  fun2cnv  6451  fun11  6454  fununi  6455  fnres  6504  mptfnf  6513  fnopabg  6515  brprcneu  6708  fvprc  6709  dffv2  6806  fvn0ssdmfun  6895  dff13  7067  eqoprab2bw  7281  eqoprab2b  7282  mpo2eqb  7342  ralrnmpo  7348  zfun  7524  uniex2  7526  funcnvuni  7709  dfer2  8392  fiint  8948  marypha1lem  9049  marypha2lem3  9053  inf2  9238  axinf2  9255  scottexs  9503  scott0s  9504  aceq1  9731  dfac4  9736  dfac7  9746  dfac0  9747  dfac1  9748  dfac10  9751  dfac10c  9752  dfac10b  9753  kmlem4  9767  kmlem12  9775  kmlem14  9777  kmlem15  9778  kmlem16  9779  dfackm  9780  ac6n  10099  axpowndlem3  10213  zfcndrep  10228  zfcndun  10229  zfcndpow  10230  axgroth5  10438  axgroth2  10439  axgroth4  10446  grothprim  10448  sstskm  10456  fimaxre3  11778  infm3  11791  nnwos  12511  cotr2g  14539  brtrclfv  14565  trclfvcotr  14572  rpnnen2lem12  15786  isprm2  16239  vdwmc2  16532  pgpfac1  19467  pgpfac  19471  iunocv  20643  2ndcdisj2  22354  hausdiag  22542  rnelfmlem  22849  alexsubALTlem3  22946  cnextfun  22961  itg2leub  24632  mptelee  26986  nmoubi  28853  nmobndseqi  28860  nmobndseqiALT  28861  isch2  29304  isch3  29322  choc0  29407  nmopub  29989  nmfnleub  30006  xfree2  30526  nelbOLD  30536  mo5f  30556  nmo  30557  reuxfrdf  30558  rabeqsnd  30567  inpr0  30599  cbvdisjf  30629  disjorf  30637  ssrelf  30674  funcnvmpt  30724  funcnv5mpt  30725  ballotlem2  32167  bnj89  32412  bnj115  32416  bnj1143  32483  bnj110  32551  bnj611  32611  bnj864  32615  bnj865  32616  bnj1000  32634  bnj978  32642  bnj1049  32667  bnj1052  32668  bnj1090  32672  bnj1030  32680  bnj1133  32682  bnj1171  32693  bnj1172  32694  bnj1174  32696  bnj1176  32698  bnj1204  32705  bnj1253  32710  bnj1388  32726  bnj1523  32764  fineqvrep  32777  fineqvpow  32778  axrepprim  33356  axunprim  33357  axpowprim  33358  axinfprim  33360  axacprim  33361  untuni  33363  fnssintima  33391  ralxp3f  33401  dffr5  33439  elintfv  33457  dfon2lem8  33485  dfon2lem9  33486  19.12b  33496  ttrclss  33519  frpoins3xpg  33524  frpoins3xp3g  33525  eqscut2  33737  brtxpsd3  33935  dfom5b  33951  dffun10  33953  bj-notalbii  34533  bj-ssbeq  34571  bj-ax12ssb  34576  bj-hbext  34629  bj-nfalt  34630  bj-substax12  34640  bj-nnfalt  34685  bj-nnfext  34686  ax11-pm2  34756  bj-sbnf  34761  bj-sblem  34765  eliminable-veqab  34787  eliminable-abeqv  34788  eliminable-abeqab  34789  bj-ralvw  34801  bj-sbeq  34823  bj-nfcf  34848  bj-snsetex  34890  bj-rcleqf  34952  fvineqsneq  35320  wl-equsalvw  35434  wl-equsalcom  35438  wl-sb8et  35445  wl-2sb6d  35450  wl-alanbii  35461  wl-sb8eut  35469  poimirlem25  35539  poimirlem30  35544  heibor1lem  35704  sbcalfi  36011  mpobi123f  36057  mptbi12f  36061  3albii  36124  ineccnvmo  36226  alrmomorn  36227  cocossss  36296  cossssid3  36324  cossssid4  36325  cosscnvssid4  36332  trcoss2  36339  dfeldisj4  36568  dfeldisj5  36569  dvelimf-o  36680  axc11n-16  36689  pmapglbx  37520  sn-axrep5v  39907  dford4  40554  rp-fakeinunass  40807  rababg  40857  elmapintrab  40860  elinintrab  40861  undmrnresiss  40888  clss2lem  40895  cotrintab  40898  elintima  40938  ss2iundf  40944  relexp0eq  40986  dfhe3  41060  snhesn  41071  psshepw  41073  dffrege76  41224  frege77  41225  frege110  41258  dffrege115  41263  frege116  41264  frege118  41266  frege131  41279  ntrneikb  41381  ismnuprim  41585  rr-grothprimbi  41586  ismnushort  41592  rr-grothshortbi  41594  pm10.541  41658  pm10.542  41659  19.21vv  41667  19.31vv  41675  19.28vv  41677  pm11.62  41685  axc11next  41697  pm13.196a  41705  2sbc6g  41706  elnev  41729  hbexgVD  42199  rabssf  42341  2rexsb  44265  dfich2  44583  ichal  44591  spr0nelg  44601  mo0sn  45834  dffun3f  46059  setrec1lem2  46065  setrec2  46072  setis  46074  alimp-surprise  46155  alimp-no-surprise  46156