Theorem raleqdv 2747

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 2741	. 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 1398   A.wral 2520

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525

This theorem is referenced by:  raleqtrdv  2749  raleqtrrdv  2751  raleqbidv  2757  raleqbidva  2759  omsinds  4744  cbvfo  5958  isoselem  5993  ofrfval  6275  issmo2  6520  smoeq  6521  tfrlemisucaccv  6556  tfr1onlemsucaccv  6572  tfrcllemsucaccv  6585  nninfisollem0  7421  isacnm  7510  fzrevral2  10440  fzrevral3  10441  fzshftral  10442  fzoshftral  10584  zsupcllemstep  10589  zsupcllemex  10590  infssuzex  10593  suprzubdc  10596  nninfdcex  10597  uzsinds  10806  iseqf1olemqk  10869  seq3f1olemstep  10876  seq3f1olemp  10877  eqs1  11316  swrdspsleq  11359  pfxeq  11388  pfxsuffeqwrdeq  11390  caucvgre  11666  cvg1nlemres  11670  rexuz3  11675  resqrexlemoverl  11706  resqrexlemsqa  11709  resqrexlemex  11710  climconst  11975  climshftlemg  11987  serf0  12037  summodclem2  12068  summodc  12069  zsumdc  12070  mertenslemi1  12221  prodmodclem2  12263  prodmodc  12264  zproddc  12265  prmind2  12817  ennnfoneleminc  13162  ennnfonelemex  13165  ennnfonelemnn0  13173  ennnfonelemr  13174  grpidpropdg  13587  sgrppropd  13626  mndpropd  13653  nmznsg  13930  ghmnsgima  13985  cmnpropd  14012  rngpropd  14099  ringpropd  14182  lsspropdg  14579  isridlrng  14630  mplvalcoe  14845  lmfval  15058  lmconst  15081  cncnp  15095  metss  15359  sin0pilem2  15647  fsumdvdsmul  15859  2sqlem10  15998  usgruspgrben  16181  wlkeq  16349  wlkl1loop  16353  uspgr2wlkeq  16360  upgr2wlkdc  16372  clwwlkccatlem  16395  clwwlknp  16412  clwwlkn1  16413  clwwlkn2  16416  nninfsellemdc  16788  nninfself  16791  nninfsellemeqinf  16794  nninfomni  16797