Theorem albii 1399

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

Syntax hints:   ↔ wb 103  ∀wal 1282

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  2albii  1400  hbxfrbi  1401  nfbii  1402  19.26-2  1411  19.26-3an  1412  alrot3  1414  alrot4  1415  albiim  1416  2albiim  1417  alnex  1428  nfalt  1510  aaanh  1518  aaan  1519  alinexa  1534  exintrbi  1564  19.21-2  1597  19.31r  1611  equsalh  1654  equsal  1655  sbcof2  1731  dvelimfALT2  1738  19.23vv  1805  sbanv  1810  pm11.53  1816  nfsbxy  1859  nfsbxyt  1860  sbcomxyyz  1887  sb9  1896  sbnf2  1898  2sb6  1901  sbcom2v  1902  sb6a  1905  2sb6rf  1907  sbalyz  1916  sbal  1917  sbal1yz  1918  sbal1  1919  sbalv  1922  2exsb  1926  nfsb4t  1931  dvelimf  1932  dveeq1  1936  sbal2  1939  sb8eu  1954  sb8euh  1964  eu1  1966  eu2  1985  mo3h  1994  moanim  2015  2eu4  2034  exists1  2037  eqcom  2083  hblem  2186  abeq2  2187  abeq1  2188  nfceqi  2215  abid2f  2243  ralbii2  2376  r2alf  2383  nfraldya  2400  r3al  2408  r19.21t  2436  r19.23t  2467  rabid2  2530  rabbi  2531  ralv  2616  ceqsralt  2626  gencbval  2647  rspc2gv  2712  ralab  2752  ralrab2  2757  euind  2779  reu2  2780  reu3  2782  rmo4  2785  reu8  2788  rmoim  2791  2reuswapdc  2794  reuind  2795  2rmorex  2796  ra5  2902  rmo2ilem  2903  rmo3  2905  dfss2  2988  ss2ab  3062  ss2rab  3070  rabss  3071  uniiunlem  3082  ddifstab  3104  ssequn1  3142  unss  3146  ralunb  3153  ssin  3188  ssddif  3198  n0rf  3260  eq0  3266  eqv  3267  rabeq0  3274  abeq0  3275  disj  3292  disj3  3296  rgenm  3343  pwss  3397  ralsnsg  3430  ralsns  3431  disjsn  3454  euabsn2  3461  snss  3516  snsssn  3553  dfnfc2  3619  uni0b  3626  unissb  3631  elintrab  3648  ssintrab  3659  intun  3667  intpr  3668  dfiin2g  3711  iunss  3719  dfdisj2  3768  cbvdisj  3776  dftr2  3877  dftr5  3878  trint  3890  zfnuleu  3902  vprc  3909  inex1  3912  repizf2lem  3935  axpweq  3945  zfpow  3949  axpow2  3950  axpow3  3951  zfpair2  3965  ssextss  3975  frirrg  4105  sucel  4165  zfun  4189  uniex2  4191  setindel  4281  setind  4282  elirr  4284  en2lp  4297  zfregfr  4316  tfi  4323  peano5  4339  ssrel  4446  ssrel2  4448  eqrelrel  4459  reliun  4476  raliunxp  4495  relop  4504  dmopab3  4566  dm0rn0  4570  reldm0  4571  cotr  4726  issref  4727  asymref  4730  intirr  4731  sb8iota  4894  dffun2  4932  dffun4  4933  dffun6f  4935  dffun4f  4938  dffun7  4948  funopab  4955  funcnv2  4979  funcnv  4980  funcnveq  4982  fun2cnv  4983  fun11  4986  fununi  4987  funcnvuni  4988  funimaexglem  5002  fnres  5035  fnopabg  5042  rexrnmpt  5331  dff13  5428  oprabidlem  5556  eqoprab2b  5583  mpt22eqb  5630  ralrnmpt2  5635  dfer2  6130  ltexprlemdisj  6796  recexprlemdisj  6820  isprm2  10499  bj-nfalt  10575  bdceq  10633  bdcriota  10674  bj-axempty2  10685  bj-vprc  10687  bdinex1  10690  bj-zfpair2  10701  bj-uniex2  10707  bj-ssom  10731  bj-inf2vnlem2  10766