Theorem albii 1820

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

Syntax hints:   ↔ wb 205  ∀wal 1538

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  2albii  1821  3albii  1822  hbxfrbi  1826  alex  1827  2nalexn  1829  2exnaln  1830  imnang  1843  alexn  1846  nfnbiOLD  1857  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  1991  equsalvw  2006  2sb6  2088  sbrimvw  2093  sbcom3vv  2097  alrot3  2156  alrot4  2157  sbal  2158  sbalv  2159  19.21-2  2201  19.32  2225  19.31  2226  equsalv  2258  sbn  2276  sbrim  2300  aaan  2327  aaanOLD  2328  pm11.53  2342  19.12vv  2343  sb8v  2348  sb8f  2349  sbievg  2359  equsal  2415  2sb6rf  2471  sbcom3  2508  sb8eulem  2596  eu1  2610  2mo2  2647  2eu1  2650  2eu1v  2651  2eu3  2653  euae  2659  nulmo  2712  abeq2w  2813  hblem  2868  hblemg  2869  abeq2  2870  abeq1  2871  nfcriOLD  2894  nfcriOLDOLD  2895  nfcriiOLD  2897  nfceqi  2901  abeq2f  2937  ralbii2  3088  r2allem  3135  r19.21vOLD  3173  r3al  3189  r19.21t  3232  r19.23t  3234  ralcom4  3265  ralcom4OLD  3266  nfra2wOLD  3279  moelOLD  3374  rabbi  3428  rabid2f  3431  rabid2OLD  3433  eqv  3450  eqvf  3451  abv  3452  abvALT  3453  ralv  3465  ceqsralt  3472  ceqsalv  3476  rspc2gv  3578  ralxpxfr2d  3585  clel2g  3598  clel4g  3603  elabgt  3613  elabg  3617  ralab  3638  ralabOLD  3639  ralrab2  3645  euind  3670  reu2  3671  reu3  3673  rmo4  3676  reu8  3679  rmo3f  3680  rmoim  3686  2reuswap  3692  2reuswap2  3693  reuind  3699  2reu5lem2  3702  2reu5lem3  3703  2rmoswap  3707  rmo2  3831  rmo3  3833  rmoanim  3838  dfss2  3918  dfss2OLD  3919  ss2ab  4004  ss2rab  4016  rabss  4017  uniiunlem  4031  dfdif3  4061  ssequn1  4127  unss  4131  ralunb  4138  ssin  4177  vn0  4285  eq0f  4287  eq0  4290  eq0ALT  4291  ssdif0  4310  inssdif0  4316  ab0w  4320  ab0  4321  ab0OLD  4322  ab0ALT  4323  ab0orv  4325  eq0rdv  4351  disj  4394  disjOLD  4395  disj3  4400  ssundif  4432  ralidmw  4452  ralidm  4456  ralf0  4458  ralf0OLD  4462  pwss  4570  rabsssn  4615  ralsnsg  4616  ralsng  4621  disjsn  4659  snssb  4730  snssgOLD  4732  pwpw0  4760  pwsnOLD  4845  dfnfc2  4877  unissb  4887  unissbOLD  4888  elintrab  4908  ssintrab  4919  intun  4928  intprg  4929  intprOLD  4931  dfiin2g  4979  iunssf  4991  iunss  4992  dfdisj2  5059  cbvdisj  5067  disjor  5072  dftr2  5211  dftr5  5213  dftr5OLD  5214  axrep1  5230  axrep5  5235  axrep6  5236  axsepgfromrep  5241  axnulALT  5248  vnex  5258  inex1  5261  axpweq  5307  zfpow  5309  axpow2  5310  axpow3  5311  nfnid  5318  dtruALT  5331  reusv2lem4  5344  zfpair2  5373  el  5382  ssextss  5398  moabex  5404  dffr6  5578  dffr2  5584  dffr2ALT  5585  dfepfr  5605  frinxp  5700  ssrel2  5727  eqrelrel  5739  reliun  5758  raliunxp  5781  relop  5792  dmopab3  5861  dm0rn0  5866  reldm0  5869  iresn0n0  5993  dffr3  6037  cotrg  6047  cotrgOLD  6048  cotrgOLDOLD  6049  idrefALT  6051  asymref  6056  asymref2  6057  intirr  6058  dffr4  6258  sucel  6375  sb8iota  6443  dffun2OLDOLD  6491  dffun6  6492  dffun3  6493  dffun3OLD  6494  dffun4  6495  dffun5  6496  dffun6f  6497  dffun7  6511  funopab  6519  funcnv2  6552  funcnv  6553  fun2cnv  6555  fun11  6558  fununi  6559  fnres  6611  mptfnf  6619  fnopabg  6621  brprcneu  6815  brprcneuALT  6816  dffv2  6919  fvn0ssdmfun  7008  dff13  7184  fnssintima  7289  eqoprab2bw  7407  eqoprab2b  7408  mpo2eqb  7468  ralrnmpo  7474  zfun  7651  uniex2  7653  funcnvuni  7846  dfer2  8570  fiint  9189  marypha1lem  9290  marypha2lem3  9294  inf2  9480  axinf2  9497  ttrclss  9577  scottexs  9744  scott0s  9745  aceq1  9974  dfac4  9979  dfac7  9989  dfac0  9990  dfac1  9991  dfac10  9994  dfac10c  9995  dfac10b  9996  kmlem4  10010  kmlem12  10018  kmlem14  10020  kmlem15  10021  kmlem16  10022  dfackm  10023  ac6n  10342  axpowndlem3  10456  zfcndrep  10471  zfcndun  10472  zfcndpow  10473  axgroth5  10681  axgroth2  10682  axgroth4  10689  grothprim  10691  sstskm  10699  fimaxre3  12022  infm3  12035  nnwos  12756  cotr2g  14786  brtrclfv  14812  trclfvcotr  14819  rpnnen2lem12  16033  isprm2  16484  vdwmc2  16777  pgpfac1  19778  pgpfac  19782  iunocv  20992  2ndcdisj2  22714  hausdiag  22902  rnelfmlem  23209  alexsubALTlem3  23306  cnextfun  23321  itg2leub  25005  eqscut2  27051  mptelee  27552  nmoubi  29422  nmobndseqi  29429  nmobndseqiALT  29430  isch2  29873  isch3  29891  choc0  29976  nmopub  30558  nmfnleub  30575  xfree2  31095  nelbOLDOLD  31105  mo5f  31125  nmo  31126  reuxfrdf  31127  rabeqsnd  31136  inpr0  31167  cbvdisjf  31197  disjorf  31205  ssrelf  31242  funcnvmpt  31291  funcnv5mpt  31292  ballotlem2  32755  bnj89  33000  bnj115  33004  bnj1143  33069  bnj110  33137  bnj611  33197  bnj864  33201  bnj865  33202  bnj1000  33220  bnj978  33228  bnj1049  33253  bnj1052  33254  bnj1090  33258  bnj1030  33266  bnj1133  33268  bnj1171  33279  bnj1172  33280  bnj1174  33282  bnj1176  33284  bnj1204  33291  bnj1253  33296  bnj1388  33312  bnj1523  33350  fineqvrep  33363  fineqvpow  33364  axrepprim  33942  axunprim  33943  axpowprim  33944  axinfprim  33946  axacprim  33947  untuni  33949  ralxp3f  33975  dffr5  34010  elintfv  34022  dfon2lem8  34049  dfon2lem9  34050  19.12b  34060  frpoins3xpg  34069  frpoins3xp3g  34070  brtxpsd3  34294  dfom5b  34310  dffun10  34312  bj-notalbii  34892  bj-ssbeq  34930  bj-ax12ssb  34935  bj-hbext  34988  bj-nfalt  34989  bj-substax12  34999  bj-nnfalt  35044  bj-nnfext  35045  ax11-pm2  35114  bj-sbnf  35119  bj-sblem  35123  eliminable-veqab  35145  eliminable-abeqv  35146  eliminable-abeqab  35147  bj-ralvw  35159  bj-sbeq  35181  bj-nfcf  35206  bj-snsetex  35247  bj-rcleqf  35309  bj-clex  35315  fvineqsneq  35696  wl-equsalvw  35810  wl-equsalcom  35814  wl-sb8et  35821  wl-2sb6d  35826  wl-alanbii  35837  wl-sb8eut  35845  poimirlem25  35915  poimirlem30  35920  heibor1lem  36080  sbcalfi  36387  mpobi123f  36433  mptbi12f  36437  ineccnvmo  36631  alrmomorn  36632  cocossss  36711  cossssid3  36744  cossssid4  36745  cosscnvssid4  36752  trcoss2  36759  dfeldisj4  36995  dfeldisj5  36996  disjres  37019  dvelimf-o  37204  axc11n-16  37213  pmapglbx  38045  sn-axrep5v  40450  dford4  41122  rp-fakeinunass  41452  rababg  41511  elmapintrab  41513  elinintrab  41514  undmrnresiss  41541  clss2lem  41548  cotrintab  41551  elintima  41590  relexp0eq  41638  dfhe3  41712  snhesn  41723  psshepw  41725  dffrege76  41876  frege77  41877  frege110  41910  dffrege115  41915  frege116  41916  frege118  41918  frege131  41931  ntrneikb  42033  ismnuprim  42241  rr-grothprimbi  42242  ismnushort  42248  rr-grothshortbi  42250  pm10.541  42314  pm10.542  42315  19.21vv  42323  19.31vv  42331  19.28vv  42333  pm11.62  42341  axc11next  42353  pm13.196a  42361  2sbc6g  42362  elnev  42385  hbexgVD  42855  rabssf  42997  2rexsb  44952  dfich2  45269  ichal  45277  spr0nelg  45287  mo0sn  46520  dffun3f  46747  setrec1lem2  46753  setrec2  46760  setis  46762  alimp-surprise  46843  alimp-no-surprise  46844