Theorem albii 1470

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

Syntax hints:   ↔ wb 105  ∀wal 1351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2albii  1471  hbxfrbi  1472  nfbii  1473  19.26-2  1482  19.26-3an  1483  alrot3  1485  alrot4  1486  albiim  1487  2albiim  1488  alnex  1499  nfalt  1578  aaanh  1586  aaan  1587  alinexa  1603  exintrbi  1633  19.21-2  1667  19.31r  1681  equsalh  1726  equsal  1727  equsalv  1793  sbcof2  1810  dvelimfALT2  1817  19.23vv  1884  sbanv  1889  pm11.53  1895  nfsbxy  1942  nfsbxyt  1943  sbcomxyyz  1972  sb9  1979  sbnf2  1981  2sb6  1984  sbcom2v  1985  sb6a  1988  2sb6rf  1990  sbalyz  1999  sbal  2000  sbal1yz  2001  sbal1  2002  sbalv  2005  2exsb  2009  nfsb4t  2014  dvelimf  2015  dveeq1  2019  sbal2  2020  sb8eu  2039  sb8euh  2049  eu1  2051  eu2  2070  mo3h  2079  moanim  2100  2eu4  2119  exists1  2122  eqcom  2179  hblem  2285  abeq2  2286  abeq1  2287  nfceqi  2315  abid2f  2345  dfrex2dc  2468  ralbii2  2487  r2alf  2494  nfraldya  2512  r3al  2521  r19.21t  2552  r19.23t  2584  rabid2  2654  rabbi  2655  ralv  2756  ceqsralt  2766  gencbval  2787  rspc2gv  2855  ralab  2899  ralrab2  2904  euind  2926  reu2  2927  reu3  2929  rmo4  2932  reu8  2935  rmo3f  2936  rmoim  2940  2reuswapdc  2943  reuind  2944  2rmorex  2945  ra5  3053  rmo2ilem  3054  rmo3  3056  dfss2  3146  ss2ab  3225  ss2rab  3233  rabss  3234  uniiunlem  3246  dfdif3  3247  ddifstab  3269  ssequn1  3307  unss  3311  ralunb  3318  ssin  3359  ssddif  3371  n0rf  3437  eq0  3443  eqv  3444  rabeq0  3454  abeq0  3455  disj  3473  disj3  3477  rgenm  3527  pwss  3593  ralsnsg  3631  ralsns  3632  disjsn  3656  euabsn2  3663  snssOLD  3720  snssb  3727  snsssn  3763  dfnfc2  3829  uni0b  3836  unissb  3841  elintrab  3858  ssintrab  3869  intun  3877  intpr  3878  dfiin2g  3921  iunss  3929  dfdisj2  3984  cbvdisj  3992  disjnim  3996  dftr2  4105  dftr5  4106  trint  4118  zfnuleu  4129  vnex  4136  inex1  4139  repizf2lem  4163  axpweq  4173  zfpow  4177  axpow2  4178  axpow3  4179  exmid01  4200  zfpair2  4212  ssextss  4222  frirrg  4352  sucel  4412  zfun  4436  uniex2  4438  setindel  4539  setind  4540  elirr  4542  en2lp  4555  zfregfr  4575  tfi  4583  peano5  4599  ssrel  4716  ssrel2  4718  eqrelrel  4729  reliun  4749  raliunxp  4770  relop  4779  dmopab3  4842  dm0rn0  4846  reldm0  4847  cotr  5012  issref  5013  asymref  5016  intirr  5017  sb8iota  5187  dffun2  5228  dffun4  5229  dffun6f  5231  dffun4f  5234  dffun7  5245  funopab  5253  funcnv2  5278  funcnv  5279  funcnveq  5281  fun2cnv  5282  fun11  5285  fununi  5286  funcnvuni  5287  funimaexglem  5301  fnres  5334  fnopabg  5341  rexrnmpt  5661  dff13  5771  oprabidlem  5908  eqoprab2b  5935  mpo2eqb  5986  ralrnmpo  5991  dfer2  6538  pw1dc0el  6913  fiintim  6930  omniwomnimkv  7167  ltexprlemdisj  7607  recexprlemdisj  7631  nnwosdc  12042  isprm2  12119  bj-stal  14586  bj-nfalt  14601  bdceq  14679  bdcriota  14720  bj-axempty2  14731  bj-vprc  14733  bdinex1  14736  bj-zfpair2  14747  bj-uniex2  14753  bj-ssom  14773  bj-inf2vnlem2  14808  ss1oel2o  14828