Theorem albii 1819

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

Syntax hints:   ↔ wb 206  ∀wal 1538

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  2albii  1820  3albii  1821  hbxfrbi  1825  alex  1826  2nalexn  1828  2exnaln  1829  imnang  1842  alexn  1845  19.26-2  1871  19.26-3an  1872  19.43OLD  1883  albiim  1889  2albiim  1890  empty  1906  19.32v  1940  19.31v  1941  19.23vv  1943  pm11.53v  1944  19.12vvv  1994  equsalvw  2004  2sb6  2087  sbrimvw  2092  sbbiiev  2093  alrot3  2161  alrot4  2162  sbal  2170  sbalv  2171  19.21-2  2210  19.32  2234  19.31  2235  equsalv  2268  sbn  2280  sbrim  2304  sbnfOLD  2312  aaan  2331  pm11.53  2344  19.12vv  2345  sb8v  2351  sb8f  2352  cbvsbvf  2361  equsal  2415  2sb6rf  2471  sbcom3  2504  sb8eulem  2591  eu1  2603  2mo2  2640  2eu1  2644  2eu1v  2645  2eu3  2647  euae  2653  nulmo  2706  eqabbw  2802  hblem  2859  hblemg  2860  eqabbOLD  2868  eqabcb  2869  nfceqi  2888  eqabf  2921  ralbii2  3071  r2allem  3121  r19.21vOLD  3159  r3al  3175  r19.21t  3231  r19.23t  3233  ralcom4  3263  cbvralsvw  3290  sbralie  3326  sbralieOLD  3328  rabbi  3436  rabid2f  3437  rabid2im  3438  eqv  3457  eqvf  3458  abv  3459  abvALT  3460  ralv  3474  ceqsralt  3482  ceqsal  3485  ceqsalv  3487  rspc2gv  3598  ralxpxfr2d  3612  clel2g  3625  clel4g  3629  elabgtOLDOLD  3640  ralab  3664  ralrab2  3669  euind  3695  reu2  3696  reu3  3698  rmo4  3701  reu8  3704  rmo3f  3705  rmoim  3711  2reuswap  3717  2reuswap2  3718  reuind  3724  2reu5lem2  3727  2reu5lem3  3728  2rmoswap  3732  sbccomlem  3832  rmo2  3850  rmo3  3852  rmoanim  3857  dfss2  3932  ss2ab  4025  ss2rab  4034  rabss  4035  uniiunlem  4050  dfdif3OLD  4081  ssequn1  4149  unss  4153  ralunb  4160  ssin  4202  vn0  4308  eq0f  4310  eq0  4313  eq0ALT  4314  ssdif0  4329  inssdif0  4337  ab0w  4342  ab0  4343  ab0ALT  4344  ab0orv  4346  eq0rdv  4370  disj  4413  disj3  4417  ssundif  4451  ralidmw  4471  ralidm  4475  ralf0  4477  pwss  4586  rabsssn  4632  rabeqsnd  4633  ralsnsg  4634  ralsng  4639  disjsn  4675  snssb  4746  snssgOLD  4748  pwpw0  4777  dfnfc2  4893  unissb  4903  unissbOLD  4904  elintrab  4924  ssintrab  4935  intun  4944  intprg  4945  dfiin2g  4996  iunssf  5008  iunss  5009  dfdisj2  5076  cbvdisj  5084  cbvdisjv  5085  disjor  5089  dftr2  5216  dftr5  5218  dftr5OLD  5219  axrep1  5235  axrep4v  5239  axrep4  5240  axrep5  5242  axrep6  5243  axrep6OLD  5244  axsepgfromrep  5249  axnulALT  5259  vnex  5269  inex1  5272  axpweq  5306  zfpow  5321  axpow2  5322  nfnid  5330  dtruALT  5343  reusv2lem4  5356  zfpair2  5388  el  5397  ssextss  5413  moabex  5419  dffr6  5594  dffr2  5599  dffr2ALT  5600  dfepfr  5622  frinxp  5721  ssrel2  5748  eqrelrel  5760  reliun  5779  raliunxp  5803  relop  5814  dmopab3  5883  dm0rn0  5888  reldm0  5891  rnopab3  5920  iresn0n0  6025  dffr3  6070  cotrg  6080  cotrgOLD  6081  cotrgOLDOLD  6082  idrefALT  6084  asymref  6089  asymref2  6090  intirr  6091  dffr4  6293  sucel  6408  sb8iota  6475  dffun2OLDOLD  6523  dffun6  6524  dffun3  6525  dffun3OLD  6526  dffun4  6527  dffun5  6528  dffun6f  6529  dffun7  6543  funopab  6551  funcnv2  6584  funcnv  6585  fun2cnv  6587  fun11  6590  fununi  6591  fnres  6645  mptfnf  6653  fnopabg  6655  brprcneu  6848  brprcneuALT  6849  dffv2  6956  fvn0ssdmfun  7046  dff13  7229  fnssintima  7337  eqoprab2bw  7459  eqoprab2b  7460  mpo2eqb  7521  ralrnmpo  7528  imaeqalov  7628  zfun  7712  uniex2  7714  funcnvuni  7908  ralxp3f  8116  frpoins3xpg  8119  frpoins3xp3g  8120  xpord3inddlem  8133  dfer2  8672  fiint  9277  fiintOLD  9278  marypha1lem  9384  marypha2lem3  9388  inf2  9576  axinf2  9593  ttrclss  9673  scottexs  9840  scott0s  9841  aceq1  10070  dfac4  10075  dfac7  10086  dfac0  10087  dfac1  10088  dfac10  10091  dfac10c  10092  dfac10b  10093  kmlem4  10107  kmlem12  10115  kmlem14  10117  kmlem15  10118  kmlem16  10119  dfackm  10120  ac6n  10438  axpowndlem3  10552  zfcndrep  10567  zfcndun  10568  zfcndpow  10569  axgroth5  10777  axgroth2  10778  axgroth4  10785  grothprim  10787  sstskm  10795  fimaxre3  12129  infm3  12142  nnwos  12874  cotr2g  14942  brtrclfv  14968  trclfvcotr  14975  rpnnen2lem12  16193  isprm2  16652  vdwmc2  16950  pgpfac1  20012  pgpfac  20016  iunocv  21590  2ndcdisj2  23344  hausdiag  23532  rnelfmlem  23839  alexsubALTlem3  23936  cnextfun  23951  itg2leub  25635  eqscut2  27718  addsuniflem  27908  mulsuniflem  28052  onsfi  28247  mptelee  28822  nmoubi  30701  nmobndseqi  30708  nmobndseqiALT  30709  isch2  31152  isch3  31170  choc0  31255  nmopub  31837  nmfnleub  31854  xfree2  32374  mo5f  32418  nmo  32419  reuxfrdf  32420  rabsspr  32430  rabsstp  32431  inpr0  32461  cbvdisjf  32500  disjorf  32508  ssrelf  32543  funcnvmpt  32591  funcnv5mpt  32592  ssdifidlprm  33429  ballotlem2  34480  bnj89  34711  bnj115  34715  bnj1143  34780  bnj110  34848  bnj611  34908  bnj864  34912  bnj865  34913  bnj1000  34931  bnj978  34939  bnj1049  34964  bnj1052  34965  bnj1090  34969  bnj1030  34977  bnj1133  34979  bnj1171  34990  bnj1172  34991  bnj1174  34993  bnj1176  34995  bnj1204  35002  bnj1253  35007  bnj1388  35023  bnj1523  35061  fineqvrep  35085  fineqvpow  35086  vonf1owev  35095  axrepprim  35689  axunprim  35690  axpowprim  35691  axinfprim  35693  axacprim  35694  untuni  35696  dffr5  35741  elintfv  35752  dfon2lem8  35778  dfon2lem9  35779  19.12b  35789  brtxpsd3  35884  dfom5b  35900  dffun10  35902  disjeq1i  36180  ss-ax8  36213  cbvdisjvw2  36223  bj-notalbii  36602  bj-ssbeq  36641  bj-ax12ssb  36646  bj-hbext  36698  bj-nfalt  36699  bj-substax12  36709  bj-nnfalt  36754  bj-nnfext  36755  ax11-pm2  36824  bj-sblem  36832  eliminable-veqab  36854  eliminable-abeqv  36855  eliminable-abeqab  36856  bj-ralvw  36867  bj-sbeq  36889  bj-nfcf  36911  bj-snsetex  36951  bj-rcleqf  37013  bj-clex  37019  fvineqsneq  37400  wl-equsalvw  37526  wl-equsalcom  37531  wl-sb9v  37537  wl-sb8eft  37539  wl-sb8et  37541  wl-2sb6d  37546  wl-alanbii  37557  wl-sb8eut  37566  wl-sb8eutv  37567  poimirlem25  37639  poimirlem30  37644  heibor1lem  37803  sbcalfi  38110  mpobi123f  38156  mptbi12f  38160  ineccnvmo  38339  alrmomorn  38340  cocossss  38427  cossssid3  38460  cossssid4  38461  cosscnvssid4  38468  trcoss2  38475  dfeldisj4  38712  dfeldisj5  38713  disjres  38736  dvelimf-o  38922  axc11n-16  38931  pmapglbx  39763  sn-axrep5v  42204  abbibw  42665  dford4  43018  unielss  43207  onsupmaxb  43228  rp-fakeinunass  43504  rababg  43563  elmapintrab  43565  elinintrab  43566  undmrnresiss  43593  clss2lem  43600  cotrintab  43603  elintima  43642  relexp0eq  43690  dfhe3  43764  snhesn  43775  psshepw  43777  dffrege76  43928  frege77  43929  frege110  43962  dffrege115  43967  frege116  43968  frege118  43970  frege131  43983  ntrneikb  44083  ismnuprim  44283  rr-grothprimbi  44284  ismnushort  44290  rr-grothshortbi  44292  pm10.541  44356  pm10.542  44357  19.21vv  44365  19.31vv  44373  19.28vv  44375  pm11.62  44383  axc11next  44395  pm13.196a  44403  2sbc6g  44404  elnev  44427  hbexgVD  44895  dfac5prim  44980  permaxext  44995  permaxrep  44996  permaxpow  44999  permac8prim  45004  rabssf  45113  sinnpoly  46892  2rexsb  47102  dfich2  47459  ichal  47467  spr0nelg  47477  mo0sn  48804  dffun3f  49671  setrec1lem2  49677  setrec2  49684  setis  49687  alimp-surprise  49769  alimp-no-surprise  49770