Theorem rsp 2591

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 2527	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1560	. 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 1396   e. wcel 2205   A.wral 2522

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

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

This theorem is referenced by:  rspa  2592  rsp2  2594  rspec  2596  r19.12  2651  ralbi  2677  rexbi  2678  reupick2  3509  dfiun2g  4025  iinss2  4046  invdisj  4104  mpteq12f  4192  trss  4219  sowlin  4443  reusv1  4581  reusv3  4583  ralxfrALT  4590  funimaexglem  5441  fun11iun  5637  fvmptssdm  5764  ffnfv  5837  riota5f  6032  mpoeq123  6114  tfri3  6600  nneneq  7113  mkvprop  7451  cauappcvgprlemladdru  7973  cauappcvgprlemladdrl  7974  caucvgprlemm  7985  suplocexprlemss  8032  suplocsrlem  8125  indstr  9928  nninfinf  10809  prodeq2  12247  fprodle  12330  bezoutlemzz  12702  sgrpidmndm  13650  srgdilem  14130  ringdilem  14173  tgcl  14946  fsumcncntop  15449  dedekindeulemlu  15503  dedekindicclemlu  15512  bj-rspgt  16575  bj-charfunr  16597