Theorem raleqdv 2692

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 2686	. 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 2468

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473

This theorem is referenced by:  raleqbidv  2698  raleqbidva  2700  omsinds  4639  cbvfo  5807  isoselem  5842  ofrfval  6115  issmo2  6314  smoeq  6315  tfrlemisucaccv  6350  tfr1onlemsucaccv  6366  tfrcllemsucaccv  6379  nninfisollem0  7158  fzrevral2  10136  fzrevral3  10137  fzshftral  10138  fzoshftral  10268  uzsinds  10473  iseqf1olemqk  10525  seq3f1olemstep  10532  seq3f1olemp  10533  caucvgre  11022  cvg1nlemres  11026  rexuz3  11031  resqrexlemoverl  11062  resqrexlemsqa  11065  resqrexlemex  11066  climconst  11330  climshftlemg  11342  serf0  11392  summodclem2  11422  summodc  11423  zsumdc  11424  mertenslemi1  11575  prodmodclem2  11617  prodmodc  11618  zproddc  11619  zsupcllemstep  11978  zsupcllemex  11979  infssuzex  11982  suprzubdc  11985  nninfdcex  11986  prmind2  12152  ennnfoneleminc  12462  ennnfonelemex  12465  ennnfonelemnn0  12473  ennnfonelemr  12474  grpidpropdg  12850  sgrppropd  12876  mndpropd  12901  nmznsg  13152  ghmnsgima  13207  cmnpropd  13234  rngpropd  13309  ringpropd  13392  lsspropdg  13747  isridlrng  13798  lmfval  14149  lmconst  14173  cncnp  14187  metss  14451  sin0pilem2  14660  2sqlem10  14930  nninfsellemdc  15218  nninfself  15221  nninfsellemeqinf  15224  nninfomni  15227