Theorem albii 1815

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

Syntax hints:   ↔ wb 206  ∀wal 1534

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  2albii  1816  3albii  1817  hbxfrbi  1821  alex  1822  2nalexn  1824  2exnaln  1825  imnang  1838  alexn  1841  nfnbiOLD  1852  19.26-2  1868  19.26-3an  1869  19.43OLD  1880  albiim  1886  2albiim  1887  empty  1903  19.32v  1937  19.31v  1938  19.23vv  1940  pm11.53v  1941  19.12vvv  1985  equsalvw  2000  2sb6  2083  sbrimvw  2088  sbbiiev  2089  alrot3  2157  alrot4  2158  sbal  2166  sbalv  2167  19.21-2  2206  19.32  2230  19.31  2231  equsalv  2264  sbn  2278  sbrim  2302  sbnfOLD  2311  aaan  2331  aaanOLD  2332  pm11.53  2346  19.12vv  2347  sb8v  2352  sb8f  2353  cbvsbvf  2363  equsal  2419  2sb6rf  2475  sbcom3  2508  sb8eulem  2595  eu1  2607  2mo2  2644  2eu1  2648  2eu1v  2649  2eu3  2651  euae  2657  nulmo  2710  eqabbw  2812  hblem  2870  hblemg  2871  eqabbOLD  2879  eqabcb  2880  nfceqi  2899  eqabf  2932  ralbii2  3086  r2allem  3139  r19.21vOLD  3178  r3al  3194  r19.21t  3250  r19.23t  3252  ralcom4  3283  ralcom4OLD  3284  nfra2wOLD  3297  cbvralsvw  3314  sbralie  3355  moelOLD  3402  rabbi  3464  rabid2f  3465  rabid2im  3466  rabid2OLD  3468  eqv  3487  eqvf  3488  abv  3489  abvALT  3490  ralv  3505  ceqsralt  3513  ceqsal  3516  ceqsalv  3518  rspc2gv  3631  ralxpxfr2d  3645  clel2g  3658  clel4g  3662  elabgtOLD  3672  elabg  3676  ralab  3699  ralabOLD  3700  ralrab2  3706  euind  3732  reu2  3733  reu3  3735  rmo4  3738  reu8  3741  rmo3f  3742  rmoim  3748  2reuswap  3754  2reuswap2  3755  reuind  3761  2reu5lem2  3764  2reu5lem3  3765  2rmoswap  3769  sbccomlem  3877  rmo2  3895  rmo3  3897  rmoanim  3902  dfss2  3980  ss2ab  4071  ss2rab  4080  rabss  4081  uniiunlem  4096  dfdif3OLD  4127  ssequn1  4195  unss  4199  ralunb  4206  ssin  4246  vn0  4350  eq0f  4352  eq0  4355  eq0ALT  4356  ssdif0  4371  inssdif0  4379  ab0w  4384  ab0  4385  ab0ALT  4386  ab0orv  4388  eq0rdv  4412  disj  4455  disj3  4459  ssundif  4493  ralidmw  4513  ralidm  4517  ralf0  4519  pwss  4627  rabsssn  4672  rabeqsnd  4673  ralsnsg  4674  ralsng  4679  disjsn  4715  snssb  4786  snssgOLD  4788  pwpw0  4817  dfnfc2  4933  unissb  4943  unissbOLD  4944  elintrab  4964  ssintrab  4975  intun  4984  intprg  4985  dfiin2g  5036  iunssf  5048  iunss  5049  dfdisj2  5116  cbvdisj  5124  cbvdisjv  5125  disjor  5129  dftr2  5266  dftr5  5268  dftr5OLD  5269  axrep1  5285  axrep4v  5289  axrep4  5290  axrep5  5292  axrep6  5293  axrep6OLD  5294  axsepgfromrep  5299  axnulALT  5309  vnex  5319  inex1  5322  axpweq  5356  zfpow  5371  axpow2  5372  axpow3  5373  nfnid  5380  dtruALT  5393  reusv2lem4  5406  zfpair2  5438  el  5447  ssextss  5463  moabex  5469  dffr6  5643  dffr2  5649  dffr2ALT  5650  dfepfr  5672  frinxp  5770  ssrel2  5797  eqrelrel  5809  reliun  5828  raliunxp  5852  relop  5863  dmopab3  5932  dm0rn0  5937  reldm0  5940  rnopab3  5969  iresn0n0  6073  dffr3  6119  cotrg  6129  cotrgOLD  6130  cotrgOLDOLD  6131  idrefALT  6133  asymref  6138  asymref2  6139  intirr  6140  dffr4  6342  sucel  6459  sb8iota  6526  dffun2OLDOLD  6574  dffun6  6575  dffun3  6576  dffun3OLD  6577  dffun4  6578  dffun5  6579  dffun6f  6580  dffun7  6594  funopab  6602  funcnv2  6635  funcnv  6636  fun2cnv  6638  fun11  6641  fununi  6642  fnres  6695  mptfnf  6703  fnopabg  6705  brprcneu  6896  brprcneuALT  6897  dffv2  7003  fvn0ssdmfun  7093  dff13  7274  fnssintima  7381  eqoprab2bw  7502  eqoprab2b  7503  mpo2eqb  7564  ralrnmpo  7571  imaeqalov  7671  zfun  7754  uniex2  7756  funcnvuni  7954  ralxp3f  8160  frpoins3xpg  8163  frpoins3xp3g  8164  xpord3inddlem  8177  dfer2  8744  fiint  9363  fiintOLD  9364  marypha1lem  9470  marypha2lem3  9474  inf2  9660  axinf2  9677  ttrclss  9757  scottexs  9924  scott0s  9925  aceq1  10154  dfac4  10159  dfac7  10170  dfac0  10171  dfac1  10172  dfac10  10175  dfac10c  10176  dfac10b  10177  kmlem4  10191  kmlem12  10199  kmlem14  10201  kmlem15  10202  kmlem16  10203  dfackm  10204  ac6n  10522  axpowndlem3  10636  zfcndrep  10651  zfcndun  10652  zfcndpow  10653  axgroth5  10861  axgroth2  10862  axgroth4  10869  grothprim  10871  sstskm  10879  fimaxre3  12211  infm3  12224  nnwos  12954  cotr2g  15011  brtrclfv  15037  trclfvcotr  15044  rpnnen2lem12  16257  isprm2  16715  vdwmc2  17012  pgpfac1  20114  pgpfac  20118  iunocv  21716  2ndcdisj2  23480  hausdiag  23668  rnelfmlem  23975  alexsubALTlem3  24072  cnextfun  24087  itg2leub  25783  eqscut2  27865  addsuniflem  28048  mulsuniflem  28189  mptelee  28924  nmoubi  30800  nmobndseqi  30807  nmobndseqiALT  30808  isch2  31251  isch3  31269  choc0  31354  nmopub  31936  nmfnleub  31953  xfree2  32473  mo5f  32516  nmo  32517  reuxfrdf  32518  rabsspr  32528  rabsstp  32529  inpr0  32557  cbvdisjf  32590  disjorf  32598  ssrelf  32634  funcnvmpt  32683  funcnv5mpt  32684  ssdifidlprm  33465  ballotlem2  34469  bnj89  34713  bnj115  34717  bnj1143  34782  bnj110  34850  bnj611  34910  bnj864  34914  bnj865  34915  bnj1000  34933  bnj978  34941  bnj1049  34966  bnj1052  34967  bnj1090  34971  bnj1030  34979  bnj1133  34981  bnj1171  34992  bnj1172  34993  bnj1174  34995  bnj1176  34997  bnj1204  35004  bnj1253  35009  bnj1388  35025  bnj1523  35063  fineqvrep  35087  fineqvpow  35088  axrepprim  35681  axunprim  35682  axpowprim  35683  axinfprim  35685  axacprim  35686  untuni  35688  dffr5  35733  elintfv  35745  dfon2lem8  35771  dfon2lem9  35772  19.12b  35782  brtxpsd3  35877  dfom5b  35893  dffun10  35895  disjeq1i  36173  ss-ax8  36207  cbvdisjvw2  36217  bj-notalbii  36596  bj-ssbeq  36635  bj-ax12ssb  36640  bj-hbext  36692  bj-nfalt  36693  bj-substax12  36703  bj-nnfalt  36748  bj-nnfext  36749  ax11-pm2  36818  bj-sblem  36826  eliminable-veqab  36848  eliminable-abeqv  36849  eliminable-abeqab  36850  bj-ralvw  36861  bj-sbeq  36883  bj-nfcf  36905  bj-snsetex  36945  bj-rcleqf  37007  bj-clex  37013  fvineqsneq  37394  wl-equsalvw  37518  wl-equsalcom  37523  wl-sb9v  37529  wl-sb8eft  37531  wl-sb8et  37533  wl-2sb6d  37538  wl-alanbii  37549  wl-sb8eut  37558  wl-sb8eutv  37559  poimirlem25  37631  poimirlem30  37636  heibor1lem  37795  sbcalfi  38102  mpobi123f  38148  mptbi12f  38152  ineccnvmo  38338  alrmomorn  38339  cocossss  38417  cossssid3  38450  cossssid4  38451  cosscnvssid4  38458  trcoss2  38465  dfeldisj4  38701  dfeldisj5  38702  disjres  38725  dvelimf-o  38910  axc11n-16  38919  pmapglbx  39751  sn-axrep5v  42233  abbibw  42663  dford4  43017  unielss  43206  onsupmaxb  43227  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  44289  rr-grothprimbi  44290  ismnushort  44296  rr-grothshortbi  44298  pm10.541  44362  pm10.542  44363  19.21vv  44371  19.31vv  44379  19.28vv  44381  pm11.62  44389  axc11next  44401  pm13.196a  44409  2sbc6g  44410  elnev  44433  hbexgVD  44903  rabssf  45058  2rexsb  47050  dfich2  47382  ichal  47390  spr0nelg  47400  mo0sn  48663  dffun3f  48912  setrec1lem2  48918  setrec2  48925  setis  48928  alimp-surprise  49010  alimp-no-surprise  49011