Theorem rsp 2597

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 2533	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1564	. 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 1400   e. wcel 2209   A.wral 2528

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

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

This theorem is referenced by:  rspa  2598  rsp2  2600  rspec  2602  r19.12  2657  ralbi  2683  rexbi  2684  reupick2  3519  dfiun2g  4039  iinss2  4060  invdisj  4118  mpteq12f  4206  trss  4233  sowlin  4460  reusv1  4599  reusv3  4601  ralxfrALT  4608  funimaexglem  5459  fun11iun  5655  fvmptssdm  5784  ffnfv  5857  riota5f  6055  mpoeq123  6137  tfri3  6628  nneneq  7148  mkvprop  7488  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  caucvgprlemm  8025  suplocexprlemss  8072  suplocsrlem  8165  indstr  9972  nninfinf  10858  prodeq2  12302  fprodle  12385  bezoutlemzz  12757  sgrpidmndm  13710  srgdilem  14247  ringdilem  14290  tgcl  15088  fsumcncntop  15591  dedekindeulemlu  15645  dedekindicclemlu  15654  bj-rspgt  16728  bj-charfunr  16750