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  5593  fvmptssdm  5719  ffnfv  5793  riota5f  5981  mpoeq123  6063  tfri3  6513  nneneq  7018  mkvprop  7325  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  caucvgprlemm  7855  suplocexprlemss  7902  suplocsrlem  7995  indstr  9788  nninfinf  10665  prodeq2  12068  fprodle  12151  bezoutlemzz  12523  sgrpidmndm  13453  srgdilem  13932  ringdilem  13975  tgcl  14738  fsumcncntop  15241  dedekindeulemlu  15295  dedekindicclemlu  15304  bj-rspgt  16150  bj-charfunr  16173