Theorem raleqdv 2737

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 2731	. 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 ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1398   A.wral 2511

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-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516

This theorem is referenced by:  raleqtrdv  2739  raleqtrrdv  2741  raleqbidv  2747  raleqbidva  2749  omsinds  4726  cbvfo  5936  isoselem  5971  ofrfval  6253  issmo2  6498  smoeq  6499  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  nninfisollem0  7389  isacnm  7478  fzrevral2  10403  fzrevral3  10404  fzshftral  10405  fzoshftral  10547  zsupcllemstep  10552  zsupcllemex  10553  infssuzex  10556  suprzubdc  10559  nninfdcex  10560  uzsinds  10769  iseqf1olemqk  10832  seq3f1olemstep  10839  seq3f1olemp  10840  eqs1  11271  swrdspsleq  11314  pfxeq  11343  pfxsuffeqwrdeq  11345  caucvgre  11621  cvg1nlemres  11625  rexuz3  11630  resqrexlemoverl  11661  resqrexlemsqa  11664  resqrexlemex  11665  climconst  11930  climshftlemg  11942  serf0  11992  summodclem2  12023  summodc  12024  zsumdc  12025  mertenslemi1  12176  prodmodclem2  12218  prodmodc  12219  zproddc  12220  prmind2  12772  ennnfoneleminc  13112  ennnfonelemex  13115  ennnfonelemnn0  13123  ennnfonelemr  13124  grpidpropdg  13537  sgrppropd  13576  mndpropd  13603  nmznsg  13880  ghmnsgima  13935  cmnpropd  13962  rngpropd  14049  ringpropd  14132  lsspropdg  14527  isridlrng  14578  mplvalcoe  14791  lmfval  15004  lmconst  15027  cncnp  15041  metss  15305  sin0pilem2  15593  fsumdvdsmul  15805  2sqlem10  15944  usgruspgrben  16127  wlkeq  16295  wlkl1loop  16299  uspgr2wlkeq  16306  upgr2wlkdc  16318  clwwlkccatlem  16341  clwwlknp  16358  clwwlkn1  16359  clwwlkn2  16362  nninfsellemdc  16736  nninfself  16739  nninfsellemeqinf  16742  nninfomni  16745