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 ) )

This proof depends on syntax axioms:   -> wi 4   A.wal 1400   e. wcel 2209   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-4 1563

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

This theorem is used by:  rspa  2598  rsp2  2600  rspec  2602  r19.12  2657  ralbi  2683  rexbi  2684  reupick2  3519  dfiun2g  4044  iinss2  4065  invdisj  4123  mpteq12f  4211  trss  4238  sowlin  4465  reusv1  4604  reusv3  4606  ralxfrALT  4613  funimaexglem  5464  fun11iun  5660  fvmptssdm  5790  ffnfv  5866  riota5f  6065  mpoeq123  6147  tfri3  6638  nneneq  7158  mkvprop  7498  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemm  8035  suplocexprlemss  8082  suplocsrlem  8175  indstr  10002  nninfinf  10893  prodeq2  12340  fprodle  12423  bezoutlemzz  12795  sgrpidmndm  13782  srgdilem  14322  ringdilem  14365  tgcl  15214  fsumcncntop  15717  dedekindeulemlu  15771  dedekindicclemlu  15780  bj-rspgt  16912  bj-charfunr  16934