Theorem albii 1523

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

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

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 1500  ax-gen 1502

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2albii  1524  hbxfrbi  1525  nfbii  1526  19.26-2  1535  19.26-3an  1536  alrot3  1538  alrot4  1539  albiim  1540  2albiim  1541  alnex  1552  nfalt  1631  aaanh  1639  aaan  1640  alinexa  1656  exintrbi  1686  19.21-2  1719  19.31r  1733  equsalh  1778  equsal  1779  equsalv  1846  sbcof2  1863  dvelimfALT2  1870  19.23vv  1937  sbanv  1944  pm11.53  1951  nfsbxy  2002  nfsbxyt  2003  sbcomxyyz  2032  sb9  2039  sbnf2  2041  2sb6  2044  sbcom2v  2045  sb6a  2048  2sb6rf  2050  sbalyz  2059  sbal  2060  sbal1yz  2061  sbal1  2062  sbalv  2065  2exsb  2069  nfsb4t  2074  dvelimf  2075  dveeq1  2079  sbal2  2080  sb8eu  2099  sb8euh  2109  eu1  2111  eu2  2131  mo3h  2140  moanim  2161  2eu4  2180  exists1  2183  eqcom  2240  hblem  2346  abeq2  2347  abeq1  2348  eqabcbw  2376  eqabcb  2377  nfceqi  2388  abid2f  2418  dfrex2dc  2541  ralbii2  2560  r2alf  2567  nfraldya  2585  r3al  2594  r19.21t  2625  r19.23t  2658  rabid2  2729  rabbi  2730  ralv  2839  ceqsralt  2849  gencbval  2871  rspc2gv  2942  ralab  2986  ralrab2  2991  euind  3013  reu2  3014  reu3  3016  rmo4  3019  reu8  3022  rmo3f  3023  rmoim  3027  2reuswapdc  3030  reuind  3031  2rmorex  3032  ra5  3141  rmo2ilem  3142  rmo3  3144  ssalel  3235  ss2ab  3316  ss2rab  3324  rabss  3325  uniiunlem  3338  dfdif3  3339  ddifstab  3361  ssequn1  3399  unss  3403  ralunb  3410  ssin  3453  ssddif  3465  n0rf  3534  eq0  3540  eqv  3541  ab0w  3550  rabeq0  3552  abeq0  3553  disj  3572  disj3  3576  pwss  3704  ralsnsg  3742  ralsns  3743  disjsn  3767  euabsn2  3776  snssOLD  3835  snssb  3843  snsssn  3881  dfnfc2  3948  uni0b  3955  unissb  3960  elintrab  3977  ssintrab  3988  intun  3996  intpr  3997  dfiin2g  4040  iunss  4048  dfdisj2  4103  cbvdisj  4111  disjnim  4115  dftr2  4226  dftr5  4227  trint  4239  zfnuleu  4252  vnex  4259  inex1  4262  repizf2lem  4293  axpweq  4303  zfpow  4307  axpow2  4308  axpow3  4309  exmid01  4330  zfpair2  4342  ssextss  4355  frirrg  4490  sucel  4550  zfun  4574  uniex2  4576  uniex2OLD  4577  setindel  4680  setind  4681  elirr  4683  en2lp  4696  zfregfr  4716  tfi  4724  peano5  4740  ssrel  4858  ssrel2  4860  eqrelrel  4871  reliun  4893  raliunxp  4916  relop  4925  dmopab3  4989  dm0rn0  4993  reldm0  4994  cotr  5164  issref  5165  asymref  5168  intirr  5169  sb8iota  5340  dffun2  5382  dffun4  5383  dffun6f  5385  dffun4f  5388  dffun7  5399  funopab  5407  funcnv2  5436  funcnv  5437  funcnveq  5439  fun2cnv  5440  fun11  5443  fununi  5444  funcnvuni  5445  funimaexglem  5459  fnres  5495  fnopabg  5502  rexrnmpt  5842  dff13  5964  iotaexel  6033  oprabidlem  6106  eqoprab2b  6136  mpo2eqb  6188  ralrnmpo  6193  dfer2  6798  pw1dc0el  7208  fiintim  7228  omniwomnimkv  7497  ltexprlemdisj  7963  recexprlemdisj  7987  nnwosdc  12794  isprm2  12873  ivthdich  15677  bj-stal  16691  bj-nfalt  16706  bdceq  16782  bdcriota  16823  bj-axempty2  16834  bj-vprc  16836  bdinex1  16839  bj-zfpair2  16850  bj-uniex2  16856  bj-ssom  16876  bj-inf2vnlem2  16911  ss1oel2o  16931