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  4233  dftr5  4234  trint  4246  zfnuleu  4259  vnex  4266  inex1  4269  repizf2lem  4300  axpweq  4310  zfpow  4314  axpow2  4315  axpow3  4316  exmid01  4337  zfpair2  4349  ssextss  4362  frirrg  4497  sucel  4557  zfun  4581  uniex2  4583  uniex2OLD  4584  setindel  4687  setind  4688  elirr  4690  en2lp  4703  zfregfr  4723  tfi  4731  peano5  4747  ssrel  4865  ssrel2  4867  eqrelrel  4878  reliun  4900  raliunxp  4923  relop  4932  dmopab3  4996  dm0rn0  5000  reldm0  5001  cotr  5172  issref  5173  asymref  5176  intirr  5177  sb8iota  5348  dffun2  5390  dffun4  5391  dffun6f  5393  dffun4f  5396  dffun7  5407  funopab  5415  funcnv2  5444  funcnv  5445  funcnveq  5447  fun2cnv  5448  fun11  5451  fununi  5452  funcnvuni  5453  funimaexglem  5467  fnres  5503  fnopabg  5510  rexrnmpt  5854  dff13  5977  iotaexel  6046  oprabidlem  6119  eqoprab2b  6149  mpo2eqb  6201  ralrnmpo  6206  dfer2  6812  pw1dc0el  7222  fiintim  7242  omniwomnimkv  7513  ltexprlemdisj  7979  recexprlemdisj  8003  nnwosdc  12841  isprm2  12920  ivthdich  15879  bj-stal  16982  bj-nfalt  16997  bdceq  17073  bdcriota  17114  bj-axempty2  17125  bj-vprc  17127  bdinex1  17130  bj-zfpair2  17141  bj-uniex2  17147  bj-ssom  17167  bj-inf2vnlem2  17202  ss1oel2o  17222  dfrals2  17337  alsbii  17348  dfralseu2  17371  alseubii  17380