Theorem raleqdv 2699

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 2693	. 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 1364   A.wral 2475

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480

This theorem is referenced by:  raleqtrdv  2701  raleqtrrdv  2703  raleqbidv  2709  raleqbidva  2711  omsinds  4659  cbvfo  5833  isoselem  5868  ofrfval  6146  issmo2  6349  smoeq  6350  tfrlemisucaccv  6385  tfr1onlemsucaccv  6401  tfrcllemsucaccv  6414  nninfisollem0  7198  fzrevral2  10184  fzrevral3  10185  fzshftral  10186  fzoshftral  10317  zsupcllemstep  10322  zsupcllemex  10323  infssuzex  10326  suprzubdc  10329  nninfdcex  10330  uzsinds  10539  iseqf1olemqk  10602  seq3f1olemstep  10609  seq3f1olemp  10610  caucvgre  11149  cvg1nlemres  11153  rexuz3  11158  resqrexlemoverl  11189  resqrexlemsqa  11192  resqrexlemex  11193  climconst  11458  climshftlemg  11470  serf0  11520  summodclem2  11550  summodc  11551  zsumdc  11552  mertenslemi1  11703  prodmodclem2  11745  prodmodc  11746  zproddc  11747  prmind2  12299  ennnfoneleminc  12639  ennnfonelemex  12642  ennnfonelemnn0  12650  ennnfonelemr  12651  grpidpropdg  13043  sgrppropd  13082  mndpropd  13107  nmznsg  13369  ghmnsgima  13424  cmnpropd  13451  rngpropd  13537  ringpropd  13620  lsspropdg  14013  isridlrng  14064  lmfval  14454  lmconst  14478  cncnp  14492  metss  14756  sin0pilem2  15044  fsumdvdsmul  15253  2sqlem10  15392  nninfsellemdc  15683  nninfself  15686  nninfsellemeqinf  15689  nninfomni  15692