Theorem rsp 2478

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 2419	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1488	. 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 1329   e. wcel 1480   A.wral 2414

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

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

This theorem is referenced by:  rsp2  2480  rspec  2482  r19.12  2536  ralbi  2562  rexbi  2563  reupick2  3357  dfiun2g  3840  iinss2  3860  invdisj  3918  mpteq12f  4003  trss  4030  sowlin  4237  reusv1  4374  reusv3  4376  ralxfrALT  4383  funimaexglem  5201  fun11iun  5381  fvmptssdm  5498  ffnfv  5571  riota5f  5747  mpoeq123  5823  tfri3  6257  nneneq  6744  mkvprop  7025  cauappcvgprlemladdru  7457  cauappcvgprlemladdrl  7458  caucvgprlemm  7469  suplocexprlemss  7516  suplocsrlem  7609  indstr  9381  prodeq2  11319  bezoutlemzz  11679  tgcl  12222  fsumcncntop  12714  dedekindeulemlu  12757  dedekindicclemlu  12766  bj-rspgt  12982