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  1988  equsalvw  2003  2sb6  2086  sbrimvw  2091  sbbiiev  2092  alrot3  2160  alrot4  2161  sbal  2169  sbalv  2170  19.21-2  2209  19.32  2233  19.31  2234  equsalv  2267  sbn  2280  sbrim  2304  sbnfOLD  2313  aaan  2332  aaanOLD  2333  pm11.53  2347  19.12vv  2348  sb8v  2354  sb8f  2355  cbvsbvf  2365  equsal  2421  2sb6rf  2477  sbcom3  2510  sb8eulem  2597  eu1  2609  2mo2  2646  2eu1  2650  2eu1v  2651  2eu3  2653  euae  2659  nulmo  2712  eqabbw  2808  hblem  2866  hblemg  2867  eqabbOLD  2875  eqabcb  2876  nfceqi  2895  eqabf  2928  ralbii2  3078  r2allem  3128  r19.21vOLD  3166  r3al  3182  r19.21t  3236  r19.23t  3238  ralcom4  3268  cbvralsvw  3296  sbralie  3337  moelOLD  3384  rabbi  3446  rabid2f  3447  rabid2im  3448  rabid2OLD  3450  eqv  3469  eqvf  3470  abv  3471  abvALT  3472  ralv  3487  ceqsralt  3495  ceqsal  3498  ceqsalv  3500  rspc2gv  3611  ralxpxfr2d  3625  clel2g  3638  clel4g  3642  elabgtOLD  3652  elabg  3655  ralab  3676  ralrab2  3681  euind  3707  reu2  3708  reu3  3710  rmo4  3713  reu8  3716  rmo3f  3717  rmoim  3723  2reuswap  3729  2reuswap2  3730  reuind  3736  2reu5lem2  3739  2reu5lem3  3740  2rmoswap  3744  sbccomlem  3844  rmo2  3862  rmo3  3864  rmoanim  3869  dfss2  3944  ss2ab  4037  ss2rab  4046  rabss  4047  uniiunlem  4062  dfdif3OLD  4093  ssequn1  4161  unss  4165  ralunb  4172  ssin  4214  vn0  4320  eq0f  4322  eq0  4325  eq0ALT  4326  ssdif0  4341  inssdif0  4349  ab0w  4354  ab0  4355  ab0ALT  4356  ab0orv  4358  eq0rdv  4382  disj  4425  disj3  4429  ssundif  4463  ralidmw  4483  ralidm  4487  ralf0  4489  pwss  4598  rabsssn  4644  rabeqsnd  4645  ralsnsg  4646  ralsng  4651  disjsn  4687  snssb  4758  snssgOLD  4760  pwpw0  4789  dfnfc2  4905  unissb  4915  unissbOLD  4916  elintrab  4936  ssintrab  4947  intun  4956  intprg  4957  dfiin2g  5008  iunssf  5020  iunss  5021  dfdisj2  5088  cbvdisj  5096  cbvdisjv  5097  disjor  5101  dftr2  5231  dftr5  5233  dftr5OLD  5234  axrep1  5250  axrep4v  5254  axrep4  5255  axrep5  5257  axrep6  5258  axrep6OLD  5259  axsepgfromrep  5264  axnulALT  5274  vnex  5284  inex1  5287  axpweq  5321  zfpow  5336  axpow2  5337  nfnid  5345  dtruALT  5358  reusv2lem4  5371  zfpair2  5403  el  5412  ssextss  5428  moabex  5434  dffr6  5609  dffr2  5615  dffr2ALT  5616  dfepfr  5638  frinxp  5737  ssrel2  5764  eqrelrel  5776  reliun  5795  raliunxp  5819  relop  5830  dmopab3  5899  dm0rn0  5904  reldm0  5907  rnopab3  5936  iresn0n0  6041  dffr3  6086  cotrg  6096  cotrgOLD  6097  cotrgOLDOLD  6098  idrefALT  6100  asymref  6105  asymref2  6106  intirr  6107  dffr4  6309  sucel  6427  sb8iota  6494  dffun2OLDOLD  6542  dffun6  6543  dffun3  6544  dffun3OLD  6545  dffun4  6546  dffun5  6547  dffun6f  6548  dffun7  6562  funopab  6570  funcnv2  6603  funcnv  6604  fun2cnv  6606  fun11  6609  fununi  6610  fnres  6664  mptfnf  6672  fnopabg  6674  brprcneu  6865  brprcneuALT  6866  dffv2  6973  fvn0ssdmfun  7063  dff13  7246  fnssintima  7354  eqoprab2bw  7475  eqoprab2b  7476  mpo2eqb  7537  ralrnmpo  7544  imaeqalov  7644  zfun  7728  uniex2  7730  funcnvuni  7926  ralxp3f  8134  frpoins3xpg  8137  frpoins3xp3g  8138  xpord3inddlem  8151  dfer2  8718  fiint  9336  fiintOLD  9337  marypha1lem  9443  marypha2lem3  9447  inf2  9635  axinf2  9652  ttrclss  9732  scottexs  9899  scott0s  9900  aceq1  10129  dfac4  10134  dfac7  10145  dfac0  10146  dfac1  10147  dfac10  10150  dfac10c  10151  dfac10b  10152  kmlem4  10166  kmlem12  10174  kmlem14  10176  kmlem15  10177  kmlem16  10178  dfackm  10179  ac6n  10497  axpowndlem3  10611  zfcndrep  10626  zfcndun  10627  zfcndpow  10628  axgroth5  10836  axgroth2  10837  axgroth4  10844  grothprim  10846  sstskm  10854  fimaxre3  12186  infm3  12199  nnwos  12929  cotr2g  14993  brtrclfv  15019  trclfvcotr  15026  rpnnen2lem12  16241  isprm2  16699  vdwmc2  16997  pgpfac1  20061  pgpfac  20065  iunocv  21639  2ndcdisj2  23393  hausdiag  23581  rnelfmlem  23888  alexsubALTlem3  23985  cnextfun  24000  itg2leub  25685  eqscut2  27768  addsuniflem  27951  mulsuniflem  28092  mptelee  28820  nmoubi  30699  nmobndseqi  30706  nmobndseqiALT  30707  isch2  31150  isch3  31168  choc0  31253  nmopub  31835  nmfnleub  31852  xfree2  32372  mo5f  32416  nmo  32417  reuxfrdf  32418  rabsspr  32428  rabsstp  32429  inpr0  32459  cbvdisjf  32498  disjorf  32506  ssrelf  32541  funcnvmpt  32591  funcnv5mpt  32592  ssdifidlprm  33419  ballotlem2  34467  bnj89  34698  bnj115  34702  bnj1143  34767  bnj110  34835  bnj611  34895  bnj864  34899  bnj865  34900  bnj1000  34918  bnj978  34926  bnj1049  34951  bnj1052  34952  bnj1090  34956  bnj1030  34964  bnj1133  34966  bnj1171  34977  bnj1172  34978  bnj1174  34980  bnj1176  34982  bnj1204  34989  bnj1253  34994  bnj1388  35010  bnj1523  35048  fineqvrep  35072  fineqvpow  35073  axrepprim  35665  axunprim  35666  axpowprim  35667  axinfprim  35669  axacprim  35670  untuni  35672  dffr5  35717  elintfv  35728  dfon2lem8  35754  dfon2lem9  35755  19.12b  35765  brtxpsd3  35860  dfom5b  35876  dffun10  35878  disjeq1i  36156  ss-ax8  36189  cbvdisjvw2  36199  bj-notalbii  36578  bj-ssbeq  36617  bj-ax12ssb  36622  bj-hbext  36674  bj-nfalt  36675  bj-substax12  36685  bj-nnfalt  36730  bj-nnfext  36731  ax11-pm2  36800  bj-sblem  36808  eliminable-veqab  36830  eliminable-abeqv  36831  eliminable-abeqab  36832  bj-ralvw  36843  bj-sbeq  36865  bj-nfcf  36887  bj-snsetex  36927  bj-rcleqf  36989  bj-clex  36995  fvineqsneq  37376  wl-equsalvw  37502  wl-equsalcom  37507  wl-sb9v  37513  wl-sb8eft  37515  wl-sb8et  37517  wl-2sb6d  37522  wl-alanbii  37533  wl-sb8eut  37542  wl-sb8eutv  37543  poimirlem25  37615  poimirlem30  37620  heibor1lem  37779  sbcalfi  38086  mpobi123f  38132  mptbi12f  38136  ineccnvmo  38321  alrmomorn  38322  cocossss  38400  cossssid3  38433  cossssid4  38434  cosscnvssid4  38441  trcoss2  38448  dfeldisj4  38684  dfeldisj5  38685  disjres  38708  dvelimf-o  38893  axc11n-16  38902  pmapglbx  39734  sn-axrep5v  42213  abbibw  42647  dford4  43000  unielss  43189  onsupmaxb  43210  rp-fakeinunass  43486  rababg  43545  elmapintrab  43547  elinintrab  43548  undmrnresiss  43575  clss2lem  43582  cotrintab  43585  elintima  43624  relexp0eq  43672  dfhe3  43746  snhesn  43757  psshepw  43759  dffrege76  43910  frege77  43911  frege110  43944  dffrege115  43949  frege116  43950  frege118  43952  frege131  43965  ntrneikb  44065  ismnuprim  44266  rr-grothprimbi  44267  ismnushort  44273  rr-grothshortbi  44275  pm10.541  44339  pm10.542  44340  19.21vv  44348  19.31vv  44356  19.28vv  44358  pm11.62  44366  axc11next  44378  pm13.196a  44386  2sbc6g  44387  elnev  44410  hbexgVD  44878  dfac5prim  44963  permaxext  44978  permaxrep  44979  permaxpow  44982  rabssf  45091  2rexsb  47078  dfich2  47420  ichal  47428  spr0nelg  47438  mo0sn  48742  dffun3f  49494  setrec1lem2  49500  setrec2  49507  setis  49510  alimp-surprise  49592  alimp-no-surprise  49593