Theorem albii 1821

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

Syntax hints:   ↔ wb 206  ∀wal 1540

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  2albii  1822  3albii  1823  hbxfrbi  1827  alex  1828  2nalexn  1830  2exnaln  1831  imnang  1844  alexn  1847  19.26-2  1873  19.26-3an  1874  19.43OLD  1885  albiim  1891  2albiim  1892  empty  1908  19.32v  1942  19.31v  1943  19.23vv  1945  pm11.53v  1946  19.12vvv  1996  equsalvw  2006  2sb6  2092  sbrimvw  2097  sbbiiev  2098  alrot3  2166  alrot4  2167  sbal  2175  sbalv  2176  19.21-2  2217  19.32  2241  19.31  2242  equsalv  2275  sbn  2287  sbrim  2311  sbnfOLD  2319  aaan  2338  pm11.53  2351  19.12vv  2352  sb8v  2358  sb8f  2359  cbvsbvf  2368  equsal  2422  2sb6rf  2478  sbcom3  2511  sb8eulem  2599  eu1  2611  2mo2  2648  2eu1  2652  2eu1v  2653  2eu3  2655  euae  2661  nulmo  2714  eqabbw  2810  eqabcbw  2811  hblem  2868  hblemg  2869  eqabcb  2877  nfceqi  2896  eqabf  2929  ralbii2  3080  r2allem  3126  r3al  3176  r19.21t  3232  r19.23t  3234  ralcom4  3264  cbvralsvw  3289  sbralie  3324  sbralieOLD  3326  rabbi  3431  rabid2f  3432  rabid2im  3433  eqv  3452  eqvf  3453  abv  3454  abvALT  3455  ralv  3469  ceqsralt  3477  ceqsal  3480  ceqsalv  3482  rspc2gv  3588  ralxpxfr2d  3602  clel2g  3615  clel4g  3619  elabgtOLDOLD  3630  ralab  3653  ralrab2  3658  euind  3684  reu2  3685  reu3  3687  rmo4  3690  reu8  3693  rmo3f  3694  rmoim  3700  2reuswap  3706  2reuswap2  3707  reuind  3713  2reu5lem2  3716  2reu5lem3  3717  2rmoswap  3721  sbccomlem  3821  rmo2  3839  rmo3  3841  rmoanim  3846  dfss2  3921  ss2ab  4015  ss2rab  4023  rabss  4024  ss2rabd  4026  uniiunlem  4041  dfdif3OLD  4072  ssequn1  4140  unss  4144  ralunb  4151  ssin  4193  eq0f  4301  eq0  4304  eq0ALT  4305  ssdif0  4320  inssdif0  4328  ab0w  4333  ab0  4334  ab0ALT  4335  ab0orv  4337  disj  4404  disj3  4408  ssundif  4442  ralf0  4452  ralidmw  4471  ralidm  4472  pwss  4579  rabsssn  4627  rabeqsnd  4628  ralsnsg  4629  ralsng  4634  disjsn  4670  snssb  4741  pwpw0  4771  dfnfc2  4887  unissb  4898  elintrab  4917  ssintrab  4928  intun  4937  intprg  4938  dfiin2g  4988  iunssf  5000  iunssfOLD  5001  iunss  5002  iunssOLD  5003  dfdisj2  5069  cbvdisj  5077  cbvdisjv  5078  disjor  5082  dftr2  5209  dftr5  5211  axrep1  5227  axrep4v  5231  axrep4  5232  axrep5  5234  axrep6  5235  axrep6OLD  5236  axsepgfromrep  5241  axnulALT  5251  vnex  5261  inex1  5264  axpweq  5298  zfpow  5313  axpow2  5314  nfnid  5322  dtruALT  5335  reusv2lem4  5348  zfpair2  5380  prex  5384  el  5394  ssextss  5408  moabexOLD  5414  dffr6  5588  dffr2  5593  dffr2ALT  5594  dfepfr  5616  frinxp  5715  ssrel2  5742  eqrelrel  5754  raliunxp  5796  relop  5807  dmopab3  5876  dm0rn0  5881  dm0rn0OLD  5882  reldm0  5885  rnopab3  5913  iresn0n0  6021  dffr3  6066  cotrg  6076  idrefALT  6078  asymref  6081  asymref2  6082  intirr  6083  dffr4  6286  sucel  6401  sb8iota  6467  dffun6  6511  dffun3  6512  dffun4  6513  dffun5  6514  dffun6f  6515  dffun7  6527  funopab  6535  funcnv2  6568  funcnv  6569  fun2cnv  6571  fun11  6574  fununi  6575  fnres  6627  mptfnf  6635  fnopabg  6637  tz6.12-2  6829  brprcneu  6832  brprcneuALT  6833  dffv2  6937  funcnvmpt  6951  fvn0ssdmfun  7028  dff13  7210  fnssintima  7318  eqoprab2bw  7438  eqoprab2b  7439  mpo2eqb  7500  ralrnmpo  7507  imaeqalov  7607  zfun  7691  uniex2  7693  funcnvuni  7884  ralxp3f  8089  frpoins3xpg  8092  frpoins3xp3g  8093  xpord3inddlem  8106  dfer2  8646  fiint  9239  marypha1lem  9348  marypha2lem3  9352  inf2  9544  axinf2  9561  ttrclss  9641  scottexs  9811  scott0s  9812  aceq1  10039  dfac4  10044  dfac7  10055  dfac0  10056  dfac1  10057  dfac10  10060  dfac10c  10061  dfac10b  10062  kmlem4  10076  kmlem12  10084  kmlem14  10086  kmlem15  10087  kmlem16  10088  dfackm  10089  ac6n  10407  axpowndlem3  10522  zfcndrep  10537  zfcndun  10538  zfcndpow  10539  axgroth5  10747  axgroth2  10748  axgroth4  10755  grothprim  10757  sstskm  10765  fimaxre3  12100  infm3  12113  nnwos  12840  cotr2g  14911  brtrclfv  14937  trclfvcotr  14944  rpnnen2lem12  16162  isprm2  16621  vdwmc2  16919  pgpfac1  20023  pgpfac  20027  iunocv  21648  2ndcdisj2  23413  hausdiag  23601  rnelfmlem  23908  alexsubALTlem3  24005  cnextfun  24020  itg2leub  25703  eqcuts2  27794  addsuniflem  28009  mulsuniflem  28157  onsfi  28364  mpteleeOLD  28980  nmoubi  30859  nmobndseqi  30866  nmobndseqiALT  30867  isch2  31310  isch3  31328  choc0  31413  nmopub  31995  nmfnleub  32012  xfree2  32532  mo5f  32574  nmo  32575  reuxfrdf  32576  rabsspr  32587  rabsstp  32588  inpr0  32618  cbvdisjf  32657  disjorf  32665  ssrelf  32704  funcnv5mpt  32756  ssdifidlprm  33550  ballotlem2  34666  bnj89  34897  bnj115  34901  bnj1143  34965  bnj110  35033  bnj611  35093  bnj864  35097  bnj865  35098  bnj1000  35116  bnj978  35124  bnj1049  35149  bnj1052  35150  bnj1090  35154  bnj1030  35162  bnj1133  35164  bnj1171  35175  bnj1172  35176  bnj1174  35178  bnj1176  35180  bnj1204  35187  bnj1253  35192  bnj1388  35208  bnj1523  35246  fineqvrep  35289  fineqvpow  35290  axreg  35302  axregscl  35303  axregs  35314  vonf1owev  35321  axrepprim  35915  axunprim  35916  axpowprim  35917  axinfprim  35919  axacprim  35920  untuni  35922  dffr5  35967  elintfv  35978  dfon2lem8  36001  dfon2lem9  36002  19.12b  36012  brtxpsd3  36107  dfom5b  36123  dffun10  36125  disjeq1i  36405  ss-ax8  36438  cbvdisjvw2  36448  mh-setind  36685  regsfromregtr  36687  regsfromsetind  36688  regsfromunir1  36689  bj-notalbii  36840  bj-cbvaew  36881  bj-df-sb  36891  bj-ssbeq  36892  bj-ax12ssb  36897  bj-hbext  36949  bj-nfalt  36950  bj-substax12  36961  bj-nnfalt  37022  bj-nnfext  37023  ax11-pm2  37078  bj-sblem  37086  eliminable-veqab  37108  eliminable-abeqv  37109  eliminable-abeqab  37110  bj-ralvw  37121  bj-sbeq  37143  bj-nfcf  37165  bj-snsetex  37205  bj-rcleqf  37267  bj-clex  37273  bj-rep  37315  bj-axseprep  37316  fvineqsneq  37661  wl-equsalvw  37787  wl-equsalcom  37792  wl-sb9v  37798  wl-sb8eft  37800  wl-sb8et  37802  wl-2sb6d  37807  wl-alanbii  37818  wl-sb8eut  37827  wl-sb8eutv  37828  poimirlem25  37890  poimirlem30  37895  heibor1lem  38054  sbcalfi  38361  mpobi123f  38407  mptbi12f  38411  ineccnvmo  38602  alrmomorn  38603  ralmo  38605  ralrmo3  38609  cocossss  38771  cossssid3  38804  cossssid4  38805  cosscnvssid4  38812  trcoss2  38819  dfeldisj4  39057  dfeldisj5  39058  disjres  39089  dvelimf-o  39299  axc11n-16  39308  pmapglbx  40139  sn-axrep5v  42583  abbibw  43029  dford4  43380  unielss  43569  onsupmaxb  43590  rp-fakeinunass  43865  rababg  43924  elmapintrab  43926  elinintrab  43927  undmrnresiss  43954  clss2lem  43961  cotrintab  43964  elintima  44003  relexp0eq  44051  dfhe3  44125  snhesn  44136  psshepw  44138  dffrege76  44289  frege77  44290  frege110  44323  dffrege115  44328  frege116  44329  frege118  44331  frege131  44344  ntrneikb  44444  ismnuprim  44644  rr-grothprimbi  44645  ismnushort  44651  rr-grothshortbi  44653  pm10.541  44717  pm10.542  44718  19.21vv  44726  19.31vv  44734  19.28vv  44736  pm11.62  44744  axc11next  44756  pm13.196a  44764  2sbc6g  44765  elnev  44787  hbexgVD  45255  dfac5prim  45340  permaxext  45355  permaxrep  45356  permaxpow  45359  permac8prim  45364  rabssf  45472  sinnpoly  47245  2rexsb  47455  dfich2  47812  ichal  47820  spr0nelg  47830  mo0sn  49169  dffun3f  50035  setrec1lem2  50041  setrec2  50048  setis  50051  alimp-surprise  50133  alimp-no-surprise  50134