Theorem rsp 2423

Description: Restricted specialization. (Contributed by NM, 17-Oct-1996.)

Assertion

Ref	Expression
rsp	|- ( A. x e. A ph -> ( x e. A -> ph ) )

Proof of Theorem rsp

Step	Hyp	Ref	Expression
1		df-ral 2364	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1446	. 2 |- ( A. x ( x e. A -> ph ) -> ( x e. A -> ph ) )
3	1, 2	sylbi 119	1 |- ( A. x e. A ph -> ( x e. A -> ph ) )

Syntax hints:   -> wi 4   A.wal 1287   e. wcel 1438   A.wral 2359

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-4 1445

This theorem depends on definitions:  df-bi 115  df-ral 2364

This theorem is referenced by:  rsp2  2425  rspec  2427  r19.12  2478  ralbi  2501  rexbi  2502  reupick2  3283  dfiun2g  3757  iinss2  3777  invdisj  3831  mpteq12f  3910  trss  3937  sowlin  4138  reusv1  4271  reusv3  4273  ralxfrALT  4280  funimaexglem  5083  fun11iun  5258  fvmptssdm  5371  ffnfv  5440  riota5f  5614  mpt2eq123  5690  tfri3  6114  nneneq  6553  cauappcvgprlemladdru  7194  cauappcvgprlemladdrl  7195  caucvgprlemm  7206  indstr  9050  bezoutlemzz  11073  bj-rspgt  11332