Theorem albii 1519

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 1517	. 2 |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> A. x ps ) )
2		albii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpg 1500	1 |- ( A. x ph <-> A. x ps )

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

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 1496  ax-gen 1498

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2albii  1520  hbxfrbi  1521  nfbii  1522  19.26-2  1531  19.26-3an  1532  alrot3  1534  alrot4  1535  albiim  1536  2albiim  1537  alnex  1548  nfalt  1627  aaanh  1635  aaan  1636  alinexa  1652  exintrbi  1682  19.21-2  1715  19.31r  1729  equsalh  1774  equsal  1775  equsalv  1842  sbcof2  1859  dvelimfALT2  1866  19.23vv  1933  sbanv  1939  pm11.53  1945  nfsbxy  1996  nfsbxyt  1997  sbcomxyyz  2026  sb9  2033  sbnf2  2035  2sb6  2038  sbcom2v  2039  sb6a  2042  2sb6rf  2044  sbalyz  2053  sbal  2054  sbal1yz  2055  sbal1  2056  sbalv  2059  2exsb  2063  nfsb4t  2068  dvelimf  2069  dveeq1  2073  sbal2  2074  sb8eu  2093  sb8euh  2103  eu1  2105  eu2  2125  mo3h  2134  moanim  2155  2eu4  2174  exists1  2177  eqcom  2234  hblem  2340  abeq2  2341  abeq1  2342  eqabcb  2369  nfceqi  2380  abid2f  2410  dfrex2dc  2533  ralbii2  2552  r2alf  2559  nfraldya  2577  r3al  2586  r19.21t  2617  r19.23t  2650  rabid2  2721  rabbi  2722  ralv  2831  ceqsralt  2841  gencbval  2863  rspc2gv  2933  ralab  2977  ralrab2  2982  euind  3004  reu2  3005  reu3  3007  rmo4  3010  reu8  3013  rmo3f  3014  rmoim  3018  2reuswapdc  3021  reuind  3022  2rmorex  3023  ra5  3132  rmo2ilem  3133  rmo3  3135  ssalel  3226  ss2ab  3306  ss2rab  3314  rabss  3315  uniiunlem  3328  dfdif3  3329  ddifstab  3351  ssequn1  3389  unss  3393  ralunb  3400  ssin  3443  ssddif  3455  n0rf  3521  eq0  3527  eqv  3528  rabeq0  3538  abeq0  3539  disj  3557  disj3  3561  pwss  3688  ralsnsg  3726  ralsns  3727  disjsn  3751  euabsn2  3760  snssOLD  3819  snssb  3827  snsssn  3865  dfnfc2  3932  uni0b  3939  unissb  3944  elintrab  3961  ssintrab  3972  intun  3980  intpr  3981  dfiin2g  4024  iunss  4032  dfdisj2  4087  cbvdisj  4095  disjnim  4099  dftr2  4210  dftr5  4211  trint  4223  zfnuleu  4234  vnex  4241  inex1  4244  repizf2lem  4274  axpweq  4284  zfpow  4288  axpow2  4289  axpow3  4290  exmid01  4311  zfpair2  4323  ssextss  4336  frirrg  4471  sucel  4531  zfun  4555  uniex2  4557  setindel  4660  setind  4661  elirr  4663  en2lp  4676  zfregfr  4696  tfi  4704  peano5  4720  ssrel  4838  ssrel2  4840  eqrelrel  4851  reliun  4873  raliunxp  4896  relop  4905  dmopab3  4969  dm0rn0  4973  reldm0  4974  cotr  5144  issref  5145  asymref  5148  intirr  5149  sb8iota  5320  dffun2  5362  dffun4  5363  dffun6f  5365  dffun4f  5368  dffun7  5379  funopab  5387  funcnv2  5416  funcnv  5417  funcnveq  5419  fun2cnv  5420  fun11  5423  fununi  5424  funcnvuni  5425  funimaexglem  5439  fnres  5475  fnopabg  5482  rexrnmpt  5820  dff13  5941  iotaexel  6008  oprabidlem  6081  eqoprab2b  6111  mpo2eqb  6163  ralrnmpo  6168  dfer2  6768  pw1dc0el  7171  fiintim  7191  omniwomnimkv  7458  ltexprlemdisj  7921  recexprlemdisj  7945  nnwosdc  12735  isprm2  12814  ivthdich  15518  bj-stal  16521  bj-nfalt  16536  bdceq  16612  bdcriota  16653  bj-axempty2  16664  bj-vprc  16666  bdinex1  16669  bj-zfpair2  16680  bj-uniex2  16686  bj-ssom  16706  bj-inf2vnlem2  16741  ss1oel2o  16761