Theorem raleqdv 2755

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 13-Nov-2005.)

Hypothesis

Ref	Expression
raleq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
raleqdv	|- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )

Distinct variable groups:   x, A   x, B

Allowed substitution hints:   ph( x)   ps( x)

Proof of Theorem raleqdv

Step	Hyp	Ref	Expression
1		raleq1d.1	. 2 |- ( ph -> A = B )
2		raleq 2749	. 2 |- ( A = B -> ( A. x e. A ps <-> A. x e. B ps ) )
3	1, 2	syl 14	1 |- ( ph -> ( A. x e. A ps <-> A. x e. B ps ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533

This theorem is used by:  raleqtrdv  2757  raleqtrrdv  2759  raleqbidv  2765  raleqbidva  2767  omsinds  4771  cbvfo  5994  isoselem  6029  ofrfval  6315  issmo2  6565  smoeq  6566  tfrlemisucaccv  6601  tfr1onlemsucaccv  6617  tfrcllemsucaccv  6630  nninfisollem0  7476  isacnm  7565  fzrevral2  10529  fzrevral3  10530  fzshftral  10531  fzoshftral  10673  zsupcllemstep  10678  zsupcllemex  10679  infssuzex  10682  suprzubdc  10687  nninfdcex  10688  uzsinds  10901  iseqf1olemqk  10964  seq3f1olemstep  10971  seq3f1olemp  10972  eqs1  11417  swrdspsleq  11460  pfxeq  11489  pfxsuffeqwrdeq  11491  caucvgre  11768  cvg1nlemres  11772  rexuz3  11777  resqrexlemoverl  11808  resqrexlemsqa  11811  resqrexlemex  11812  climconst  12080  climshftlemg  12092  serf0  12142  summodclem2  12173  summodc  12174  zsumdc  12175  mertenslemi1  12326  prodmodclem2  12368  prodmodc  12369  zproddc  12370  prmind2  12922  ennnfoneleminc  13359  ennnfonelemex  13362  ennnfonelemnn0  13370  ennnfonelemr  13371  grpidpropdg  13752  sgrppropd  13786  mndpropd  13811  nmznsg  14074  ghmnsgima  14129  cmnpropd  14187  rngpropd  14360  ringpropd  14449  lsspropdg  14876  isridlrng  14927  isassa  15110  assapropd  15122  lmfval  15436  lmconst  15459  cncnp  15473  metss  15737  sin0pilem2  16026  fsumdvdsmul  16302  chtqub  16313  2sqlem10  16466  usgruspgrben  16649  wlkeq  16817  wlkl1loop  16821  uspgr2wlkeq  16828  upgr2wlkdc  16840  clwwlkccatlem  16863  clwwlknp  16880  clwwlkn1  16881  clwwlkn2  16884  nninfsellemdc  17276  nninfself  17279  nninfsellemeqinf  17282  nninfomni  17285