Theorem raleqdv 2734

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 2728	. 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 1395   A.wral 2508

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513

This theorem is referenced by:  raleqtrdv  2736  raleqtrrdv  2738  raleqbidv  2744  raleqbidva  2746  omsinds  4714  cbvfo  5915  isoselem  5950  ofrfval  6233  issmo2  6441  smoeq  6442  tfrlemisucaccv  6477  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  nninfisollem0  7308  isacnm  7396  fzrevral2  10314  fzrevral3  10315  fzshftral  10316  fzoshftral  10456  zsupcllemstep  10461  zsupcllemex  10462  infssuzex  10465  suprzubdc  10468  nninfdcex  10469  uzsinds  10678  iseqf1olemqk  10741  seq3f1olemstep  10748  seq3f1olemp  10749  eqs1  11176  swrdspsleq  11215  pfxeq  11244  pfxsuffeqwrdeq  11246  caucvgre  11508  cvg1nlemres  11512  rexuz3  11517  resqrexlemoverl  11548  resqrexlemsqa  11551  resqrexlemex  11552  climconst  11817  climshftlemg  11829  serf0  11879  summodclem2  11909  summodc  11910  zsumdc  11911  mertenslemi1  12062  prodmodclem2  12104  prodmodc  12105  zproddc  12106  prmind2  12658  ennnfoneleminc  12998  ennnfonelemex  13001  ennnfonelemnn0  13009  ennnfonelemr  13010  grpidpropdg  13423  sgrppropd  13462  mndpropd  13489  nmznsg  13766  ghmnsgima  13821  cmnpropd  13848  rngpropd  13934  ringpropd  14017  lsspropdg  14411  isridlrng  14462  mplvalcoe  14670  lmfval  14883  lmconst  14906  cncnp  14920  metss  15184  sin0pilem2  15472  fsumdvdsmul  15681  2sqlem10  15820  usgruspgrben  16000  wlkeq  16100  wlkl1loop  16104  uspgr2wlkeq  16111  upgr2wlkdc  16121  clwwlkccatlem  16143  clwwlknp  16159  clwwlkn1  16160  clwwlkn2  16163  nninfsellemdc  16464  nninfself  16467  nninfsellemeqinf  16470  nninfomni  16473