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  5926  isoselem  5961  ofrfval  6244  issmo2  6455  smoeq  6456  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  nninfisollem0  7329  isacnm  7418  fzrevral2  10341  fzrevral3  10342  fzshftral  10343  fzoshftral  10484  zsupcllemstep  10489  zsupcllemex  10490  infssuzex  10493  suprzubdc  10496  nninfdcex  10497  uzsinds  10706  iseqf1olemqk  10769  seq3f1olemstep  10776  seq3f1olemp  10777  eqs1  11205  swrdspsleq  11248  pfxeq  11277  pfxsuffeqwrdeq  11279  caucvgre  11542  cvg1nlemres  11546  rexuz3  11551  resqrexlemoverl  11582  resqrexlemsqa  11585  resqrexlemex  11586  climconst  11851  climshftlemg  11863  serf0  11913  summodclem2  11944  summodc  11945  zsumdc  11946  mertenslemi1  12097  prodmodclem2  12139  prodmodc  12140  zproddc  12141  prmind2  12693  ennnfoneleminc  13033  ennnfonelemex  13036  ennnfonelemnn0  13044  ennnfonelemr  13045  grpidpropdg  13458  sgrppropd  13497  mndpropd  13524  nmznsg  13801  ghmnsgima  13856  cmnpropd  13883  rngpropd  13970  ringpropd  14053  lsspropdg  14447  isridlrng  14498  mplvalcoe  14706  lmfval  14919  lmconst  14942  cncnp  14956  metss  15220  sin0pilem2  15508  fsumdvdsmul  15717  2sqlem10  15856  usgruspgrben  16039  wlkeq  16207  wlkl1loop  16211  uspgr2wlkeq  16218  upgr2wlkdc  16230  clwwlkccatlem  16253  clwwlknp  16270  clwwlkn1  16271  clwwlkn2  16274  nninfsellemdc  16615  nninfself  16618  nninfsellemeqinf  16621  nninfomni  16624