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  4212  trss  4240  sowlin  4467  reusv1  4606  reusv3  4608  ralxfrALT  4615  funimaexglem  5467  fun11iun  5663  fvmptssdm  5793  ffnfv  5869  riota5f  6068  mpoeq123  6150  tfri3  6643  nneneq  7164  mkvprop  7504  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemm  8041  suplocexprlemss  8088  suplocsrlem  8181  indstr  10008  nninfinf  10900  prodeq2  12348  fprodle  12431  bezoutlemzz  12803  sgrpidmndm  13791  srgdilem  14379  ringdilem  14422  tgcl  15307  fsumcncntop  15810  dedekindeulemlu  15864  dedekindicclemlu  15873  bj-rspgt  17036  bj-charfunr  17058