Theorem albii 1822

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

Syntax hints:   ↔ wb 205  ∀wal 1540

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  2albii  1823  3albii  1824  hbxfrbi  1828  alex  1829  2nalexn  1831  2exnaln  1832  imnang  1845  alexn  1848  nfnbiOLD  1859  19.26-2  1875  19.26-3an  1876  19.43OLD  1887  albiim  1893  2albiim  1894  empty  1910  19.32v  1944  19.31v  1945  19.23vv  1947  pm11.53v  1948  19.12vvv  1993  equsalvw  2008  2sb6  2090  sbrimvw  2095  sbcom3vv  2099  alrot3  2158  alrot4  2159  sbal  2160  sbalv  2161  19.21-2  2203  19.32  2227  19.31  2228  equsalv  2259  sbn  2277  sbrim  2301  aaan  2328  aaanOLD  2329  pm11.53  2343  19.12vv  2344  sb8v  2349  sb8f  2350  cbvsbvf  2361  equsal  2417  2sb6rf  2473  sbcom3  2506  sb8eulem  2593  eu1  2607  2mo2  2644  2eu1  2647  2eu1v  2648  2eu3  2650  euae  2656  nulmo  2709  eqabbw  2810  hblem  2866  hblemg  2867  eqabbOLD  2875  eqabcb  2876  nfcriOLD  2894  nfcriOLDOLD  2895  nfcriiOLD  2897  nfceqi  2901  eqabf  2936  ralbii2  3090  r2allem  3143  r19.21vOLD  3181  r3al  3197  r19.21t  3251  r19.23t  3253  ralcom4  3284  ralcom4OLD  3285  nfra2wOLD  3298  sbralie  3355  moelOLD  3402  rabbi  3463  rabid2f  3464  rabid2OLD  3466  eqv  3484  eqvf  3485  abv  3486  abvALT  3487  ralv  3499  ceqsralt  3507  ceqsal  3510  ceqsalv  3512  rspc2gv  3622  ralxpxfr2d  3635  clel2g  3648  clel4g  3653  elabgt  3663  elabg  3667  ralab  3688  ralabOLD  3689  ralrab2  3695  euind  3721  reu2  3722  reu3  3724  rmo4  3727  reu8  3730  rmo3f  3731  rmoim  3737  2reuswap  3743  2reuswap2  3744  reuind  3750  2reu5lem2  3753  2reu5lem3  3754  2rmoswap  3758  rmo2  3882  rmo3  3884  rmoanim  3889  dfss2  3969  dfss2OLD  3970  ss2ab  4057  ss2rab  4069  rabss  4070  uniiunlem  4085  dfdif3  4115  ssequn1  4181  unss  4185  ralunb  4192  ssin  4231  vn0  4339  eq0f  4341  eq0  4344  eq0ALT  4345  ssdif0  4364  inssdif0  4370  ab0w  4374  ab0  4375  ab0OLD  4376  ab0ALT  4377  ab0orv  4379  eq0rdv  4405  disj  4448  disjOLD  4449  disj3  4454  ssundif  4488  ralidmw  4508  ralidm  4512  ralf0  4514  ralf0OLD  4518  pwss  4626  rabsssn  4671  rabeqsnd  4672  ralsnsg  4673  ralsng  4678  disjsn  4716  snssb  4787  snssgOLD  4789  pwpw0  4817  pwsnOLD  4902  dfnfc2  4934  unissb  4944  unissbOLD  4945  elintrab  4965  ssintrab  4976  intun  4985  intprg  4986  intprOLD  4988  dfiin2g  5036  iunssf  5048  iunss  5049  dfdisj2  5116  cbvdisj  5124  disjor  5129  dftr2  5268  dftr5  5270  dftr5OLD  5271  axrep1  5287  axrep5  5292  axrep6  5293  axsepgfromrep  5298  axnulALT  5305  vnex  5315  inex1  5318  axpweq  5349  zfpow  5365  axpow2  5366  axpow3  5367  nfnid  5374  dtruALT  5387  reusv2lem4  5400  zfpair2  5429  el  5438  ssextss  5454  moabex  5460  dffr6  5635  dffr2  5641  dffr2ALT  5642  dfepfr  5662  frinxp  5759  ssrel2  5786  eqrelrel  5798  reliun  5817  raliunxp  5840  relop  5851  dmopab3  5920  dm0rn0  5925  reldm0  5928  iresn0n0  6054  dffr3  6099  cotrg  6109  cotrgOLD  6110  cotrgOLDOLD  6111  idrefALT  6113  asymref  6118  asymref2  6119  intirr  6120  dffr4  6321  sucel  6439  sb8iota  6508  dffun2OLDOLD  6556  dffun6  6557  dffun3  6558  dffun3OLD  6559  dffun4  6560  dffun5  6561  dffun6f  6562  dffun7  6576  funopab  6584  funcnv2  6617  funcnv  6618  fun2cnv  6620  fun11  6623  fununi  6624  fnres  6678  mptfnf  6686  fnopabg  6688  brprcneu  6882  brprcneuALT  6883  dffv2  6987  fvn0ssdmfun  7077  dff13  7254  fnssintima  7359  eqoprab2bw  7479  eqoprab2b  7480  mpo2eqb  7541  ralrnmpo  7547  imaeqalov  7646  zfun  7726  uniex2  7728  funcnvuni  7922  ralxp3f  8123  frpoins3xpg  8126  frpoins3xp3g  8127  xpord3inddlem  8140  dfer2  8704  fiint  9324  marypha1lem  9428  marypha2lem3  9432  inf2  9618  axinf2  9635  ttrclss  9715  scottexs  9882  scott0s  9883  aceq1  10112  dfac4  10117  dfac7  10127  dfac0  10128  dfac1  10129  dfac10  10132  dfac10c  10133  dfac10b  10134  kmlem4  10148  kmlem12  10156  kmlem14  10158  kmlem15  10159  kmlem16  10160  dfackm  10161  ac6n  10480  axpowndlem3  10594  zfcndrep  10609  zfcndun  10610  zfcndpow  10611  axgroth5  10819  axgroth2  10820  axgroth4  10827  grothprim  10829  sstskm  10837  fimaxre3  12160  infm3  12173  nnwos  12899  cotr2g  14923  brtrclfv  14949  trclfvcotr  14956  rpnnen2lem12  16168  isprm2  16619  vdwmc2  16912  pgpfac1  19950  pgpfac  19954  iunocv  21234  2ndcdisj2  22961  hausdiag  23149  rnelfmlem  23456  alexsubALTlem3  23553  cnextfun  23568  itg2leub  25252  eqscut2  27307  addsuniflem  27484  mulsuniflem  27604  mptelee  28153  nmoubi  30025  nmobndseqi  30032  nmobndseqiALT  30033  isch2  30476  isch3  30494  choc0  30579  nmopub  31161  nmfnleub  31178  xfree2  31698  mo5f  31729  nmo  31730  reuxfrdf  31731  inpr0  31769  cbvdisjf  31802  disjorf  31810  ssrelf  31844  funcnvmpt  31892  funcnv5mpt  31893  ballotlem2  33487  bnj89  33732  bnj115  33736  bnj1143  33801  bnj110  33869  bnj611  33929  bnj864  33933  bnj865  33934  bnj1000  33952  bnj978  33960  bnj1049  33985  bnj1052  33986  bnj1090  33990  bnj1030  33998  bnj1133  34000  bnj1171  34011  bnj1172  34012  bnj1174  34014  bnj1176  34016  bnj1204  34023  bnj1253  34028  bnj1388  34044  bnj1523  34082  fineqvrep  34095  fineqvpow  34096  axrepprim  34671  axunprim  34672  axpowprim  34673  axinfprim  34675  axacprim  34676  untuni  34678  dffr5  34724  elintfv  34736  dfon2lem8  34762  dfon2lem9  34763  19.12b  34773  brtxpsd3  34868  dfom5b  34884  dffun10  34886  bj-notalbii  35492  bj-ssbeq  35530  bj-ax12ssb  35535  bj-hbext  35588  bj-nfalt  35589  bj-substax12  35599  bj-nnfalt  35644  bj-nnfext  35645  ax11-pm2  35714  bj-sbnf  35719  bj-sblem  35723  eliminable-veqab  35745  eliminable-abeqv  35746  eliminable-abeqab  35747  bj-ralvw  35759  bj-sbeq  35781  bj-nfcf  35803  bj-snsetex  35844  bj-rcleqf  35906  bj-clex  35912  fvineqsneq  36293  wl-equsalvw  36407  wl-equsalcom  36411  wl-sb8et  36418  wl-2sb6d  36423  wl-alanbii  36434  wl-sb8eut  36442  poimirlem25  36513  poimirlem30  36518  heibor1lem  36677  sbcalfi  36984  mpobi123f  37030  mptbi12f  37034  ineccnvmo  37226  alrmomorn  37227  cocossss  37306  cossssid3  37339  cossssid4  37340  cosscnvssid4  37347  trcoss2  37354  dfeldisj4  37590  dfeldisj5  37591  disjres  37614  dvelimf-o  37799  axc11n-16  37808  pmapglbx  38640  sn-axrep5v  41033  dford4  41768  unielss  41967  onsupmaxb  41988  rp-fakeinunass  42266  rababg  42325  elmapintrab  42327  elinintrab  42328  undmrnresiss  42355  clss2lem  42362  cotrintab  42365  elintima  42404  relexp0eq  42452  dfhe3  42526  snhesn  42537  psshepw  42539  dffrege76  42690  frege77  42691  frege110  42724  dffrege115  42729  frege116  42730  frege118  42732  frege131  42745  ntrneikb  42845  ismnuprim  43053  rr-grothprimbi  43054  ismnushort  43060  rr-grothshortbi  43062  pm10.541  43126  pm10.542  43127  19.21vv  43135  19.31vv  43143  19.28vv  43145  pm11.62  43153  axc11next  43165  pm13.196a  43173  2sbc6g  43174  elnev  43197  hbexgVD  43667  rabssf  43808  2rexsb  45809  dfich2  46126  ichal  46134  spr0nelg  46144  mo0sn  47500  dffun3f  47727  setrec1lem2  47733  setrec2  47740  setis  47743  alimp-surprise  47827  alimp-no-surprise  47828