Theorem rspcva 2699

Description: Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.)

Hypothesis

Ref	Expression
rspcv.1	|- ( x = A -> ( ph <-> ps ) )

Assertion

Ref	Expression
rspcva	|- ( ( A e. B /\ A. x e. B ph ) -> ps )

Distinct variable groups:   x, A   x, B   ps, x

Allowed substitution hint:   ph( x)

Proof of Theorem rspcva

Step	Hyp	Ref	Expression
1		rspcv.1	. . 3 |- ( x = A -> ( ph <-> ps ) )
2	1	rspcv 2697	. 2 |- ( A e. B -> ( A. x e. B ph -> ps ) )
3	2	imp 122	1 |- ( ( A e. B /\ A. x e. B ph ) -> ps )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   = wceq 1284   e. wcel 1433   A.wral 2348

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353  df-v 2603

This theorem is referenced by:  tfisi  4328  suppssov1  5729  caofinvl  5753  tfrlem1  5946  supmoti  6406  caucvgsrlemgt1  6971  peano2nnnn  7021  axcaucvglemcau  7064  squeeze0  7982  peano2nn  8051  nnsub  8077  zextle  8438  rexuz3  9876  cau3lem  10000  caubnd2  10003  climcn1  10147  serif0  10189  dvdsext  10255