Theorem raleqdv 2679

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 2673	. 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 1353   A.wral 2455

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460

This theorem is referenced by:  raleqbidv  2685  raleqbidva  2687  omsinds  4623  cbvfo  5788  isoselem  5823  ofrfval  6093  issmo2  6292  smoeq  6293  tfrlemisucaccv  6328  tfr1onlemsucaccv  6344  tfrcllemsucaccv  6357  nninfisollem0  7130  fzrevral2  10108  fzrevral3  10109  fzshftral  10110  fzoshftral  10240  uzsinds  10444  iseqf1olemqk  10496  seq3f1olemstep  10503  seq3f1olemp  10504  caucvgre  10992  cvg1nlemres  10996  rexuz3  11001  resqrexlemoverl  11032  resqrexlemsqa  11035  resqrexlemex  11036  climconst  11300  climshftlemg  11312  serf0  11362  summodclem2  11392  summodc  11393  zsumdc  11394  mertenslemi1  11545  prodmodclem2  11587  prodmodc  11588  zproddc  11589  zsupcllemstep  11948  zsupcllemex  11949  infssuzex  11952  suprzubdc  11955  nninfdcex  11956  prmind2  12122  ennnfoneleminc  12414  ennnfonelemex  12417  ennnfonelemnn0  12425  ennnfonelemr  12426  grpidpropdg  12798  mndpropd  12846  nmznsg  13078  cmnpropd  13103  ringpropd  13222  lmfval  13731  lmconst  13755  cncnp  13769  metss  14033  sin0pilem2  14242  2sqlem10  14511  nninfsellemdc  14798  nninfself  14801  nninfsellemeqinf  14804  nninfomni  14807