Theorem rsp 2544

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 2480	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1525	. 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 1362   e. wcel 2167   A.wral 2475

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

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

This theorem is referenced by:  rspa  2545  rsp2  2547  rspec  2549  r19.12  2603  ralbi  2629  rexbi  2630  reupick2  3450  dfiun2g  3949  iinss2  3970  invdisj  4028  mpteq12f  4114  trss  4141  sowlin  4356  reusv1  4494  reusv3  4496  ralxfrALT  4503  funimaexglem  5342  fun11iun  5526  fvmptssdm  5647  ffnfv  5721  riota5f  5903  mpoeq123  5982  tfri3  6426  nneneq  6919  mkvprop  7225  cauappcvgprlemladdru  7725  cauappcvgprlemladdrl  7726  caucvgprlemm  7737  suplocexprlemss  7784  suplocsrlem  7877  indstr  9669  nninfinf  10537  prodeq2  11724  fprodle  11807  bezoutlemzz  12179  sgrpidmndm  13071  srgdilem  13535  ringdilem  13578  tgcl  14310  fsumcncntop  14813  dedekindeulemlu  14867  dedekindicclemlu  14876  bj-rspgt  15442  bj-charfunr  15466