Theorem rsp 2439

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 2380	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1456	. 2 |- ( A. x ( x e. A -> ph ) -> ( x e. A -> ph ) )
3	1, 2	sylbi 120	1 |- ( A. x e. A ph -> ( x e. A -> ph ) )

Syntax hints:   -> wi 4   A.wal 1297   e. wcel 1448   A.wral 2375

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

This theorem depends on definitions:  df-bi 116  df-ral 2380

This theorem is referenced by:  rsp2  2441  rspec  2443  r19.12  2497  ralbi  2523  rexbi  2524  reupick2  3309  dfiun2g  3792  iinss2  3812  invdisj  3869  mpteq12f  3948  trss  3975  sowlin  4180  reusv1  4317  reusv3  4319  ralxfrALT  4326  funimaexglem  5142  fun11iun  5322  fvmptssdm  5437  ffnfv  5510  riota5f  5686  mpoeq123  5762  tfri3  6194  nneneq  6680  mkvprop  6943  cauappcvgprlemladdru  7365  cauappcvgprlemladdrl  7366  caucvgprlemm  7377  indstr  9238  bezoutlemzz  11483  tgcl  12015  bj-rspgt  12574