Theorem albii 1481

Description: Inference adding universal quantifier to both sides of an equivalence. (Contributed by NM, 7-Aug-1994.)

Hypothesis

Ref	Expression
albii.1	|- ( ph <-> ps )

Assertion

Ref	Expression
albii	|- ( A. x ph <-> A. x ps )

Proof of Theorem albii

Step	Hyp	Ref	Expression
1		albi 1479	. 2 |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> A. x ps ) )
2		albii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpg 1462	1 |- ( A. x ph <-> A. x ps )

Syntax hints:   <-> wb 105   A.wal 1362

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 1458  ax-gen 1460

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2albii  1482  hbxfrbi  1483  nfbii  1484  19.26-2  1493  19.26-3an  1494  alrot3  1496  alrot4  1497  albiim  1498  2albiim  1499  alnex  1510  nfalt  1589  aaanh  1597  aaan  1598  alinexa  1614  exintrbi  1644  19.21-2  1678  19.31r  1692  equsalh  1737  equsal  1738  equsalv  1804  sbcof2  1821  dvelimfALT2  1828  19.23vv  1895  sbanv  1901  pm11.53  1907  nfsbxy  1958  nfsbxyt  1959  sbcomxyyz  1988  sb9  1995  sbnf2  1997  2sb6  2000  sbcom2v  2001  sb6a  2004  2sb6rf  2006  sbalyz  2015  sbal  2016  sbal1yz  2017  sbal1  2018  sbalv  2021  2exsb  2025  nfsb4t  2030  dvelimf  2031  dveeq1  2035  sbal2  2036  sb8eu  2055  sb8euh  2065  eu1  2067  eu2  2086  mo3h  2095  moanim  2116  2eu4  2135  exists1  2138  eqcom  2195  hblem  2301  abeq2  2302  abeq1  2303  nfceqi  2332  abid2f  2362  dfrex2dc  2485  ralbii2  2504  r2alf  2511  nfraldya  2529  r3al  2538  r19.21t  2569  r19.23t  2601  rabid2  2671  rabbi  2672  ralv  2777  ceqsralt  2787  gencbval  2808  rspc2gv  2876  ralab  2920  ralrab2  2925  euind  2947  reu2  2948  reu3  2950  rmo4  2953  reu8  2956  rmo3f  2957  rmoim  2961  2reuswapdc  2964  reuind  2965  2rmorex  2966  ra5  3074  rmo2ilem  3075  rmo3  3077  dfss2  3168  ss2ab  3247  ss2rab  3255  rabss  3256  uniiunlem  3268  dfdif3  3269  ddifstab  3291  ssequn1  3329  unss  3333  ralunb  3340  ssin  3381  ssddif  3393  n0rf  3459  eq0  3465  eqv  3466  rabeq0  3476  abeq0  3477  disj  3495  disj3  3499  pwss  3617  ralsnsg  3655  ralsns  3656  disjsn  3680  euabsn2  3687  snssOLD  3744  snssb  3751  snsssn  3787  dfnfc2  3853  uni0b  3860  unissb  3865  elintrab  3882  ssintrab  3893  intun  3901  intpr  3902  dfiin2g  3945  iunss  3953  dfdisj2  4008  cbvdisj  4016  disjnim  4020  dftr2  4129  dftr5  4130  trint  4142  zfnuleu  4153  vnex  4160  inex1  4163  repizf2lem  4190  axpweq  4200  zfpow  4204  axpow2  4205  axpow3  4206  exmid01  4227  zfpair2  4239  ssextss  4249  frirrg  4381  sucel  4441  zfun  4465  uniex2  4467  setindel  4570  setind  4571  elirr  4573  en2lp  4586  zfregfr  4606  tfi  4614  peano5  4630  ssrel  4747  ssrel2  4749  eqrelrel  4760  reliun  4780  raliunxp  4803  relop  4812  dmopab3  4875  dm0rn0  4879  reldm0  4880  cotr  5047  issref  5048  asymref  5051  intirr  5052  sb8iota  5222  dffun2  5264  dffun4  5265  dffun6f  5267  dffun4f  5270  dffun7  5281  funopab  5289  funcnv2  5314  funcnv  5315  funcnveq  5317  fun2cnv  5318  fun11  5321  fununi  5322  funcnvuni  5323  funimaexglem  5337  fnres  5370  fnopabg  5377  rexrnmpt  5701  dff13  5811  iotaexel  5878  oprabidlem  5949  eqoprab2b  5976  mpo2eqb  6028  ralrnmpo  6033  dfer2  6588  pw1dc0el  6967  fiintim  6985  omniwomnimkv  7226  ltexprlemdisj  7666  recexprlemdisj  7690  nnwosdc  12176  isprm2  12255  ivthdich  14807  bj-stal  15241  bj-nfalt  15256  bdceq  15334  bdcriota  15375  bj-axempty2  15386  bj-vprc  15388  bdinex1  15391  bj-zfpair2  15402  bj-uniex2  15408  bj-ssom  15428  bj-inf2vnlem2  15463  ss1oel2o  15484