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 )

This proof depends on syntax axioms:   <-> wb 105   A.wal 1400

This proof depends on 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 proof depends on definitions:  df-bi 117

This theorem is used 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  3573  disj3  3577  pwss  3708  ralsnsg  3746  ralsns  3747  disjsn  3771  euabsn2  3780  snssOLD  3840  snssb  3848  snsssn  3886  dfnfc2  3953  uni0b  3960  unissb  3965  elintrab  3982  ssintrab  3993  intun  4001  intpr  4002  dfiin2g  4045  iunss  4053  dfdisj2  4108  cbvdisj  4116  disjnim  4120  dftr2  4231  dftr5  4232  trint  4244  zfnuleu  4257  vnex  4264  inex1  4267  repizf2lem  4298  axpweq  4308  zfpow  4312  axpow2  4313  axpow3  4314  exmid01  4335  zfpair2  4347  ssextss  4360  frirrg  4495  sucel  4555  zfun  4579  uniex2  4581  uniex2OLD  4582  setindel  4685  setind  4686  elirr  4688  en2lp  4701  zfregfr  4721  tfi  4729  peano5  4745  ssrel  4863  ssrel2  4865  eqrelrel  4876  reliun  4898  raliunxp  4921  relop  4930  dmopab3  4994  dm0rn0  4998  reldm0  4999  cotr  5169  issref  5170  asymref  5173  intirr  5174  sb8iota  5345  dffun2  5387  dffun4  5388  dffun6f  5390  dffun4f  5393  dffun7  5404  funopab  5412  funcnv2  5441  funcnv  5442  funcnveq  5444  fun2cnv  5445  fun11  5448  fununi  5449  funcnvuni  5450  funimaexglem  5464  fnres  5500  fnopabg  5507  rexrnmpt  5851  dff13  5974  iotaexel  6043  oprabidlem  6116  eqoprab2b  6146  mpo2eqb  6198  ralrnmpo  6203  dfer2  6808  pw1dc0el  7218  fiintim  7238  omniwomnimkv  7507  ltexprlemdisj  7973  recexprlemdisj  7997  nnwosdc  12816  isprm2  12895  ivthdich  15754  bj-stal  16777  bj-nfalt  16792  bdceq  16868  bdcriota  16909  bj-axempty2  16920  bj-vprc  16922  bdinex1  16925  bj-zfpair2  16936  bj-uniex2  16942  bj-ssom  16962  bj-inf2vnlem2  16997  ss1oel2o  17017  dfrals2  17130  alsbii  17141  dfralseu2  17164  alseubii  17173