Theorem rsp 2577

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 2513	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1557	. 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 1393   e. wcel 2200   A.wral 2508

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

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

This theorem is referenced by:  rspa  2578  rsp2  2580  rspec  2582  r19.12  2637  ralbi  2663  rexbi  2664  reupick2  3490  dfiun2g  3997  iinss2  4018  invdisj  4076  mpteq12f  4164  trss  4191  sowlin  4411  reusv1  4549  reusv3  4551  ralxfrALT  4558  funimaexglem  5404  fun11iun  5595  fvmptssdm  5721  ffnfv  5795  riota5f  5987  mpoeq123  6069  tfri3  6519  nneneq  7026  mkvprop  7336  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprlemm  7866  suplocexprlemss  7913  suplocsrlem  8006  indstr  9800  nninfinf  10677  prodeq2  12084  fprodle  12167  bezoutlemzz  12539  sgrpidmndm  13469  srgdilem  13948  ringdilem  13991  tgcl  14754  fsumcncntop  15257  dedekindeulemlu  15311  dedekindicclemlu  15320  bj-rspgt  16233  bj-charfunr  16256