Theorem raleqdv 2666

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 2660	. 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 104   = wceq 1343   A.wral 2443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-cleq 2158  df-clel 2161  df-nfc 2296  df-ral 2448

This theorem is referenced by:  raleqbidv  2672  raleqbidva  2674  omsinds  4598  cbvfo  5752  isoselem  5787  ofrfval  6057  issmo2  6253  smoeq  6254  tfrlemisucaccv  6289  tfr1onlemsucaccv  6305  tfrcllemsucaccv  6318  nninfisollem0  7090  fzrevral2  10037  fzrevral3  10038  fzshftral  10039  fzoshftral  10169  uzsinds  10373  iseqf1olemqk  10425  seq3f1olemstep  10432  seq3f1olemp  10433  caucvgre  10919  cvg1nlemres  10923  rexuz3  10928  resqrexlemoverl  10959  resqrexlemsqa  10962  resqrexlemex  10963  climconst  11227  climshftlemg  11239  serf0  11289  summodclem2  11319  summodc  11320  zsumdc  11321  mertenslemi1  11472  prodmodclem2  11514  prodmodc  11515  zproddc  11516  zsupcllemstep  11874  zsupcllemex  11875  infssuzex  11878  suprzubdc  11881  nninfdcex  11882  prmind2  12048  ennnfoneleminc  12340  ennnfonelemex  12343  ennnfonelemnn0  12351  ennnfonelemr  12352  lmfval  12792  lmconst  12816  cncnp  12830  metss  13094  sin0pilem2  13303  2sqlem10  13561  nninfsellemdc  13850  nninfself  13853  nninfsellemeqinf  13856  nninfomni  13859