Theorem raleqdv 2755

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 2749	. 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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533

This theorem is used by:  raleqtrdv  2757  raleqtrrdv  2759  raleqbidv  2765  raleqbidva  2767  omsinds  4769  cbvfo  5991  isoselem  6026  ofrfval  6311  issmo2  6560  smoeq  6561  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  nninfisollem0  7470  isacnm  7559  fzrevral2  10523  fzrevral3  10524  fzshftral  10525  fzoshftral  10667  zsupcllemstep  10672  zsupcllemex  10673  infssuzex  10676  suprzubdc  10681  nninfdcex  10682  uzsinds  10894  iseqf1olemqk  10957  seq3f1olemstep  10964  seq3f1olemp  10965  eqs1  11410  swrdspsleq  11453  pfxeq  11482  pfxsuffeqwrdeq  11484  caucvgre  11761  cvg1nlemres  11765  rexuz3  11770  resqrexlemoverl  11801  resqrexlemsqa  11804  resqrexlemex  11805  climconst  12072  climshftlemg  12084  serf0  12134  summodclem2  12165  summodc  12166  zsumdc  12167  mertenslemi1  12318  prodmodclem2  12360  prodmodc  12361  zproddc  12362  prmind2  12914  ennnfoneleminc  13351  ennnfonelemex  13354  ennnfonelemnn0  13362  ennnfonelemr  13363  grpidpropdg  13743  sgrppropd  13777  mndpropd  13802  nmznsg  14065  ghmnsgima  14120  cmnpropd  14147  rngpropd  14303  ringpropd  14392  lsspropdg  14817  isridlrng  14868  isassa  15051  assapropd  15063  mplvalcoe  15130  lmfval  15343  lmconst  15366  cncnp  15380  metss  15644  sin0pilem2  15933  fsumdvdsmul  16186  2sqlem10  16342  usgruspgrben  16525  wlkeq  16693  wlkl1loop  16697  uspgr2wlkeq  16704  upgr2wlkdc  16716  clwwlkccatlem  16739  clwwlknp  16756  clwwlkn1  16757  clwwlkn2  16760  nninfsellemdc  17151  nninfself  17154  nninfsellemeqinf  17157  nninfomni  17160