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 205  ∀wal 1537

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 206

This theorem is referenced by:  2albii  1820  3albii  1821  hbxfrbi  1825  alex  1826  2nalexn  1828  2exnaln  1829  imnang  1842  alexn  1845  nfnbiOLD  1856  19.26-2  1872  19.26-3an  1873  19.43OLD  1884  albiim  1890  2albiim  1891  empty  1907  19.32v  1941  19.31v  1942  19.23vv  1944  pm11.53v  1945  19.12vvv  1990  equsalvw  2005  2sb6  2087  sbrimvw  2092  sbcom3vv  2096  alrot3  2155  alrot4  2156  sbal  2157  sbalv  2158  19.21-2  2200  19.32  2224  19.31  2225  equsalv  2256  sbn  2274  sbrim  2298  aaan  2325  aaanOLD  2326  pm11.53  2340  19.12vv  2341  sb8v  2346  sb8f  2347  cbvsbvf  2358  equsal  2414  2sb6rf  2470  sbcom3  2503  sb8eulem  2590  eu1  2604  2mo2  2641  2eu1  2644  2eu1v  2645  2eu3  2647  euae  2653  nulmo  2706  eqabbw  2807  hblem  2863  hblemg  2864  eqabbOLD  2872  eqabcb  2873  nfcriOLD  2891  nfcriOLDOLD  2892  nfcriiOLD  2894  nfceqi  2898  eqabf  2933  ralbii2  3087  r2allem  3140  r19.21vOLD  3178  r3al  3194  r19.21t  3248  r19.23t  3250  ralcom4  3281  ralcom4OLD  3282  nfra2wOLD  3295  sbralie  3352  moelOLD  3399  rabbi  3460  rabid2f  3461  rabid2OLD  3463  eqv  3481  eqvf  3482  abv  3483  abvALT  3484  ralv  3497  ceqsralt  3505  ceqsal  3508  ceqsalv  3510  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  7258  fnssintima  7363  eqoprab2bw  7483  eqoprab2b  7484  mpo2eqb  7545  ralrnmpo  7551  imaeqalov  7650  zfun  7730  uniex2  7732  funcnvuni  7926  ralxp3f  8127  frpoins3xpg  8130  frpoins3xp3g  8131  xpord3inddlem  8144  dfer2  8708  fiint  9328  marypha1lem  9432  marypha2lem3  9436  inf2  9622  axinf2  9639  ttrclss  9719  scottexs  9886  scott0s  9887  aceq1  10116  dfac4  10121  dfac7  10131  dfac0  10132  dfac1  10133  dfac10  10136  dfac10c  10137  dfac10b  10138  kmlem4  10152  kmlem12  10160  kmlem14  10162  kmlem15  10163  kmlem16  10164  dfackm  10165  ac6n  10484  axpowndlem3  10598  zfcndrep  10613  zfcndun  10614  zfcndpow  10615  axgroth5  10823  axgroth2  10824  axgroth4  10831  grothprim  10833  sstskm  10841  fimaxre3  12166  infm3  12179  nnwos  12905  cotr2g  14929  brtrclfv  14955  trclfvcotr  14962  rpnnen2lem12  16174  isprm2  16625  vdwmc2  16918  pgpfac1  19993  pgpfac  19997  iunocv  21455  2ndcdisj2  23183  hausdiag  23371  rnelfmlem  23678  alexsubALTlem3  23775  cnextfun  23790  itg2leub  25486  eqscut2  27542  addsuniflem  27721  mulsuniflem  27841  mptelee  28418  nmoubi  30290  nmobndseqi  30297  nmobndseqiALT  30298  isch2  30741  isch3  30759  choc0  30844  nmopub  31426  nmfnleub  31443  xfree2  31963  mo5f  31994  nmo  31995  reuxfrdf  31996  inpr0  32034  cbvdisjf  32067  disjorf  32075  ssrelf  32109  funcnvmpt  32157  funcnv5mpt  32158  ballotlem2  33783  bnj89  34028  bnj115  34032  bnj1143  34097  bnj110  34165  bnj611  34225  bnj864  34229  bnj865  34230  bnj1000  34248  bnj978  34256  bnj1049  34281  bnj1052  34282  bnj1090  34286  bnj1030  34294  bnj1133  34296  bnj1171  34307  bnj1172  34308  bnj1174  34310  bnj1176  34312  bnj1204  34319  bnj1253  34324  bnj1388  34340  bnj1523  34378  fineqvrep  34391  fineqvpow  34392  axrepprim  34973  axunprim  34974  axpowprim  34975  axinfprim  34977  axacprim  34978  untuni  34980  dffr5  35026  elintfv  35038  dfon2lem8  35064  dfon2lem9  35065  19.12b  35075  brtxpsd3  35170  dfom5b  35186  dffun10  35188  bj-notalbii  35797  bj-ssbeq  35835  bj-ax12ssb  35840  bj-hbext  35893  bj-nfalt  35894  bj-substax12  35904  bj-nnfalt  35949  bj-nnfext  35950  ax11-pm2  36019  bj-sbnf  36024  bj-sblem  36028  eliminable-veqab  36050  eliminable-abeqv  36051  eliminable-abeqab  36052  bj-ralvw  36064  bj-sbeq  36086  bj-nfcf  36108  bj-snsetex  36149  bj-rcleqf  36211  bj-clex  36217  fvineqsneq  36598  wl-equsalvw  36712  wl-equsalcom  36716  wl-sb8et  36723  wl-2sb6d  36728  wl-alanbii  36739  wl-sb8eut  36747  poimirlem25  36818  poimirlem30  36823  heibor1lem  36982  sbcalfi  37289  mpobi123f  37335  mptbi12f  37339  ineccnvmo  37531  alrmomorn  37532  cocossss  37611  cossssid3  37644  cossssid4  37645  cosscnvssid4  37652  trcoss2  37659  dfeldisj4  37895  dfeldisj5  37896  disjres  37919  dvelimf-o  38104  axc11n-16  38113  pmapglbx  38945  sn-axrep5v  41341  dford4  42072  unielss  42271  onsupmaxb  42292  rp-fakeinunass  42570  rababg  42629  elmapintrab  42631  elinintrab  42632  undmrnresiss  42659  clss2lem  42666  cotrintab  42669  elintima  42708  relexp0eq  42756  dfhe3  42830  snhesn  42841  psshepw  42843  dffrege76  42994  frege77  42995  frege110  43028  dffrege115  43033  frege116  43034  frege118  43036  frege131  43049  ntrneikb  43149  ismnuprim  43357  rr-grothprimbi  43358  ismnushort  43364  rr-grothshortbi  43366  pm10.541  43430  pm10.542  43431  19.21vv  43439  19.31vv  43447  19.28vv  43449  pm11.62  43457  axc11next  43469  pm13.196a  43477  2sbc6g  43478  elnev  43501  hbexgVD  43971  rabssf  44111  2rexsb  46109  dfich2  46426  ichal  46434  spr0nelg  46444  mo0sn  47589  dffun3f  47816  setrec1lem2  47822  setrec2  47829  setis  47832  alimp-surprise  47916  alimp-no-surprise  47917