Theorem raleqdv 2736

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 2730	. 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 1397   A.wral 2510

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515

This theorem is referenced by:  raleqtrdv  2738  raleqtrrdv  2740  raleqbidv  2746  raleqbidva  2748  omsinds  4720  cbvfo  5925  isoselem  5960  ofrfval  6243  issmo2  6454  smoeq  6455  tfrlemisucaccv  6490  tfr1onlemsucaccv  6506  tfrcllemsucaccv  6519  nninfisollem0  7328  isacnm  7417  fzrevral2  10340  fzrevral3  10341  fzshftral  10342  fzoshftral  10483  zsupcllemstep  10488  zsupcllemex  10489  infssuzex  10492  suprzubdc  10495  nninfdcex  10496  uzsinds  10705  iseqf1olemqk  10768  seq3f1olemstep  10775  seq3f1olemp  10776  eqs1  11204  swrdspsleq  11247  pfxeq  11276  pfxsuffeqwrdeq  11278  caucvgre  11541  cvg1nlemres  11545  rexuz3  11550  resqrexlemoverl  11581  resqrexlemsqa  11584  resqrexlemex  11585  climconst  11850  climshftlemg  11862  serf0  11912  summodclem2  11942  summodc  11943  zsumdc  11944  mertenslemi1  12095  prodmodclem2  12137  prodmodc  12138  zproddc  12139  prmind2  12691  ennnfoneleminc  13031  ennnfonelemex  13034  ennnfonelemnn0  13042  ennnfonelemr  13043  grpidpropdg  13456  sgrppropd  13495  mndpropd  13522  nmznsg  13799  ghmnsgima  13854  cmnpropd  13881  rngpropd  13967  ringpropd  14050  lsspropdg  14444  isridlrng  14495  mplvalcoe  14703  lmfval  14916  lmconst  14939  cncnp  14953  metss  15217  sin0pilem2  15505  fsumdvdsmul  15714  2sqlem10  15853  usgruspgrben  16036  wlkeq  16204  wlkl1loop  16208  uspgr2wlkeq  16215  upgr2wlkdc  16227  clwwlkccatlem  16250  clwwlknp  16267  clwwlkn1  16268  clwwlkn2  16271  nninfsellemdc  16612  nninfself  16615  nninfsellemeqinf  16618  nninfomni  16621