Theorem albii 1457

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

Syntax hints:   ↔ wb 104  ∀wal 1340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2albii  1458  hbxfrbi  1459  nfbii  1460  19.26-2  1469  19.26-3an  1470  alrot3  1472  alrot4  1473  albiim  1474  2albiim  1475  alnex  1486  nfalt  1565  aaanh  1573  aaan  1574  alinexa  1590  exintrbi  1620  19.21-2  1654  19.31r  1668  equsalh  1713  equsal  1714  equsalv  1780  sbcof2  1797  dvelimfALT2  1804  19.23vv  1871  sbanv  1876  pm11.53  1882  nfsbxy  1929  nfsbxyt  1930  sbcomxyyz  1959  sb9  1966  sbnf2  1968  2sb6  1971  sbcom2v  1972  sb6a  1975  2sb6rf  1977  sbalyz  1986  sbal  1987  sbal1yz  1988  sbal1  1989  sbalv  1992  2exsb  1996  nfsb4t  2001  dvelimf  2002  dveeq1  2006  sbal2  2007  sb8eu  2026  sb8euh  2036  eu1  2038  eu2  2057  mo3h  2066  moanim  2087  2eu4  2106  exists1  2109  eqcom  2166  hblem  2272  abeq2  2273  abeq1  2274  nfceqi  2302  abid2f  2332  dfrex2dc  2455  ralbii2  2474  r2alf  2481  nfraldya  2499  r3al  2508  r19.21t  2539  r19.23t  2571  rabid2  2640  rabbi  2641  ralv  2738  ceqsralt  2748  gencbval  2769  rspc2gv  2837  ralab  2881  ralrab2  2886  euind  2908  reu2  2909  reu3  2911  rmo4  2914  reu8  2917  rmo3f  2918  rmoim  2922  2reuswapdc  2925  reuind  2926  2rmorex  2927  ra5  3034  rmo2ilem  3035  rmo3  3037  dfss2  3126  ss2ab  3205  ss2rab  3213  rabss  3214  uniiunlem  3226  dfdif3  3227  ddifstab  3249  ssequn1  3287  unss  3291  ralunb  3298  ssin  3339  ssddif  3351  n0rf  3416  eq0  3422  eqv  3423  rabeq0  3433  abeq0  3434  disj  3452  disj3  3456  rgenm  3506  pwss  3569  ralsnsg  3607  ralsns  3608  disjsn  3632  euabsn2  3639  snss  3696  snsssn  3735  dfnfc2  3801  uni0b  3808  unissb  3813  elintrab  3830  ssintrab  3841  intun  3849  intpr  3850  dfiin2g  3893  iunss  3901  dfdisj2  3955  cbvdisj  3963  disjnim  3967  dftr2  4076  dftr5  4077  trint  4089  zfnuleu  4100  vnex  4107  inex1  4110  repizf2lem  4134  axpweq  4144  zfpow  4148  axpow2  4149  axpow3  4150  exmid01  4171  zfpair2  4182  ssextss  4192  frirrg  4322  sucel  4382  zfun  4406  uniex2  4408  setindel  4509  setind  4510  elirr  4512  en2lp  4525  zfregfr  4545  tfi  4553  peano5  4569  ssrel  4686  ssrel2  4688  eqrelrel  4699  reliun  4719  raliunxp  4739  relop  4748  dmopab3  4811  dm0rn0  4815  reldm0  4816  cotr  4979  issref  4980  asymref  4983  intirr  4984  sb8iota  5154  dffun2  5192  dffun4  5193  dffun6f  5195  dffun4f  5198  dffun7  5209  funopab  5217  funcnv2  5242  funcnv  5243  funcnveq  5245  fun2cnv  5246  fun11  5249  fununi  5250  funcnvuni  5251  funimaexglem  5265  fnres  5298  fnopabg  5305  rexrnmpt  5622  dff13  5730  oprabidlem  5864  eqoprab2b  5891  mpo2eqb  5942  ralrnmpo  5947  dfer2  6493  pw1dc0el  6868  fiintim  6885  omniwomnimkv  7122  ltexprlemdisj  7538  recexprlemdisj  7562  isprm2  12028  bj-stal  13464  bj-nfalt  13480  bdceq  13559  bdcriota  13600  bj-axempty2  13611  bj-vprc  13613  bdinex1  13616  bj-zfpair2  13627  bj-uniex2  13633  bj-ssom  13653  bj-inf2vnlem2  13688  ss1oel2o  13707