Theorem rsp 2553

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 2489	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1534	. 2 |- ( A. x ( x e. A -> ph ) -> ( x e. A -> ph ) )
3	1, 2	sylbi 121	1 |- ( A. x e. A ph -> ( x e. A -> ph ) )

Syntax hints:   -> wi 4   A.wal 1371   e. wcel 2176   A.wral 2484

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

This theorem depends on definitions:  df-bi 117  df-ral 2489

This theorem is referenced by:  rspa  2554  rsp2  2556  rspec  2558  r19.12  2612  ralbi  2638  rexbi  2639  reupick2  3459  dfiun2g  3959  iinss2  3980  invdisj  4038  mpteq12f  4125  trss  4152  sowlin  4368  reusv1  4506  reusv3  4508  ralxfrALT  4515  funimaexglem  5358  fun11iun  5545  fvmptssdm  5666  ffnfv  5740  riota5f  5926  mpoeq123  6006  tfri3  6455  nneneq  6956  mkvprop  7262  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  caucvgprlemm  7783  suplocexprlemss  7830  suplocsrlem  7923  indstr  9716  nninfinf  10590  prodeq2  11901  fprodle  11984  bezoutlemzz  12356  sgrpidmndm  13285  srgdilem  13764  ringdilem  13807  tgcl  14569  fsumcncntop  15072  dedekindeulemlu  15126  dedekindicclemlu  15135  bj-rspgt  15759  bj-charfunr  15783