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  5909  isoselem  5944  ofrfval  6227  issmo2  6435  smoeq  6436  tfrlemisucaccv  6471  tfr1onlemsucaccv  6487  tfrcllemsucaccv  6500  nninfisollem0  7297  isacnm  7385  fzrevral2  10302  fzrevral3  10303  fzshftral  10304  fzoshftral  10444  zsupcllemstep  10449  zsupcllemex  10450  infssuzex  10453  suprzubdc  10456  nninfdcex  10457  uzsinds  10666  iseqf1olemqk  10729  seq3f1olemstep  10736  seq3f1olemp  10737  eqs1  11161  swrdspsleq  11199  pfxeq  11228  pfxsuffeqwrdeq  11230  caucvgre  11492  cvg1nlemres  11496  rexuz3  11501  resqrexlemoverl  11532  resqrexlemsqa  11535  resqrexlemex  11536  climconst  11801  climshftlemg  11813  serf0  11863  summodclem2  11893  summodc  11894  zsumdc  11895  mertenslemi1  12046  prodmodclem2  12088  prodmodc  12089  zproddc  12090  prmind2  12642  ennnfoneleminc  12982  ennnfonelemex  12985  ennnfonelemnn0  12993  ennnfonelemr  12994  grpidpropdg  13407  sgrppropd  13446  mndpropd  13473  nmznsg  13750  ghmnsgima  13805  cmnpropd  13832  rngpropd  13918  ringpropd  14001  lsspropdg  14395  isridlrng  14446  mplvalcoe  14654  lmfval  14867  lmconst  14890  cncnp  14904  metss  15168  sin0pilem2  15456  fsumdvdsmul  15665  2sqlem10  15804  usgruspgrben  15984  wlkeq  16065  wlkl1loop  16069  uspgr2wlkeq  16076  nninfsellemdc  16376  nninfself  16379  nninfsellemeqinf  16382  nninfomni  16385