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  7471  isacnm  7560  fzrevral2  10524  fzrevral3  10525  fzshftral  10526  fzoshftral  10668  zsupcllemstep  10673  zsupcllemex  10674  infssuzex  10677  suprzubdc  10682  nninfdcex  10683  uzsinds  10896  iseqf1olemqk  10959  seq3f1olemstep  10966  seq3f1olemp  10967  eqs1  11412  swrdspsleq  11455  pfxeq  11484  pfxsuffeqwrdeq  11486  caucvgre  11763  cvg1nlemres  11767  rexuz3  11772  resqrexlemoverl  11803  resqrexlemsqa  11806  resqrexlemex  11807  climconst  12075  climshftlemg  12087  serf0  12137  summodclem2  12168  summodc  12169  zsumdc  12170  mertenslemi1  12321  prodmodclem2  12363  prodmodc  12364  zproddc  12365  prmind2  12917  ennnfoneleminc  13354  ennnfonelemex  13357  ennnfonelemnn0  13365  ennnfonelemr  13366  grpidpropdg  13747  sgrppropd  13781  mndpropd  13806  nmznsg  14069  ghmnsgima  14124  cmnpropd  14182  rngpropd  14338  ringpropd  14427  lsspropdg  14852  isridlrng  14903  isassa  15086  assapropd  15098  mplvalcoe  15172  lmfval  15385  lmconst  15408  cncnp  15422  metss  15686  sin0pilem2  15975  fsumdvdsmul  16246  chtqub  16257  2sqlem10  16410  usgruspgrben  16593  wlkeq  16761  wlkl1loop  16765  uspgr2wlkeq  16772  upgr2wlkdc  16784  clwwlkccatlem  16807  clwwlknp  16824  clwwlkn1  16825  clwwlkn2  16828  nninfsellemdc  17219  nninfself  17222  nninfsellemeqinf  17225  nninfomni  17228