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  4124  trss  4151  sowlin  4367  reusv1  4505  reusv3  4507  ralxfrALT  4514  funimaexglem  5357  fun11iun  5543  fvmptssdm  5664  ffnfv  5738  riota5f  5924  mpoeq123  6004  tfri3  6453  nneneq  6954  mkvprop  7260  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  caucvgprlemm  7781  suplocexprlemss  7828  suplocsrlem  7921  indstr  9714  nninfinf  10588  prodeq2  11868  fprodle  11951  bezoutlemzz  12323  sgrpidmndm  13252  srgdilem  13731  ringdilem  13774  tgcl  14536  fsumcncntop  15039  dedekindeulemlu  15093  dedekindicclemlu  15102  bj-rspgt  15722  bj-charfunr  15746