Theorem albii 1359

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

Syntax hints:   ↔ wb 98  ∀wal 1241

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  2albii  1360  hbxfrbi  1361  nfbii  1362  19.26-2  1371  19.26-3an  1372  alrot3  1374  alrot4  1375  albiim  1376  2albiim  1377  alnex  1388  nfalt  1470  aaanh  1478  aaan  1479  alinexa  1494  exintrbi  1524  19.21-2  1557  19.31r  1571  equsalh  1614  equsal  1615  sbcof2  1691  dvelimfALT2  1698  19.23vv  1764  sbanv  1769  pm11.53  1775  nfsbxy  1818  nfsbxyt  1819  sbcomxyyz  1846  sb9  1855  sbnf2  1857  2sb6  1860  sbcom2v  1861  sb6a  1864  2sb6rf  1866  sbalyz  1875  sbal  1876  sbal1yz  1877  sbal1  1878  sbalv  1881  2exsb  1885  nfsb4t  1890  dvelimf  1891  dveeq1  1895  sbal2  1898  sb8eu  1913  sb8euh  1923  eu1  1925  eu2  1944  mo3h  1953  moanim  1974  2eu4  1993  exists1  1996  eqcom  2042  hblem  2145  abeq2  2146  abeq1  2147  nfceqi  2174  abid2f  2202  ralbii2  2331  r2alf  2338  nfraldya  2355  r3al  2363  r19.21t  2391  r19.23t  2420  rabid2  2483  rabbi  2484  ralv  2568  ceqsralt  2578  gencbval  2599  ralab  2698  ralrab2  2703  euind  2725  reu2  2726  reu3  2728  rmo4  2731  reu8  2734  rmoim  2737  2reuswapdc  2740  reuind  2741  2rmorex  2742  ra5  2843  rmo2ilem  2844  rmo3  2846  dfss2  2931  ss2ab  3005  ss2rab  3013  rabss  3014  uniiunlem  3025  ssequn1  3110  unss  3114  ralunb  3121  ssin  3156  ssddif  3168  n0rf  3230  eq0  3236  eqv  3237  rabeq0  3244  abeq0  3245  disj  3265  disj3  3269  rgenm  3320  pwss  3371  ralsnsg  3404  ralsns  3405  disjsn  3429  euabsn2  3436  snss  3491  snsssn  3529  dfnfc2  3595  uni0b  3602  unissb  3607  elintrab  3624  ssintrab  3635  intun  3643  intpr  3644  dfiin2g  3687  iunss  3695  dfdisj2  3744  cbvdisj  3752  dftr2  3853  dftr5  3854  trint  3866  zfnuleu  3878  vprc  3885  inex1  3888  repizf2lem  3911  axpweq  3921  zfpow  3925  axpow2  3926  axpow3  3927  zfpair2  3942  ssextss  3953  frirrg  4082  sucel  4134  zfun  4158  uniex2  4160  setindel  4248  setind  4249  elirr  4251  en2lp  4263  tfi  4283  peano5  4299  ssrel  4406  ssrel2  4408  eqrelrel  4419  reliun  4436  raliunxp  4455  relop  4464  dmopab3  4526  dm0rn0  4530  reldm0  4531  cotr  4684  issref  4685  asymref  4688  intirr  4689  sb8iota  4852  dffun2  4890  dffun4  4891  dffun6f  4893  dffun4f  4896  dffun7  4906  funopab  4913  funcnv2  4937  funcnv  4938  funcnveq  4940  fun2cnv  4941  fun11  4944  fununi  4945  funcnvuni  4946  funimaexglem  4960  fnres  4993  fnopabg  5000  rexrnmpt  5288  dff13  5385  oprabidlem  5514  eqoprab2b  5541  mpt22eqb  5588  ralrnmpt2  5593  dfer2  6085  ltexprlemdisj  6676  recexprlemdisj  6700  bj-nfalt  9768  bdceq  9826  bdcriota  9867  bj-axempty2  9878  bj-vprc  9880  bdinex1  9883  bj-zfpair2  9894  bj-uniex2  9900  bj-ssom  9924  peano5setOLD  9929  bj-inf2vnlem2  9960