Theorem rsp 2555

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 2491	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1535	. 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 2178   A.wral 2486

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

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

This theorem is referenced by:  rspa  2556  rsp2  2558  rspec  2560  r19.12  2614  ralbi  2640  rexbi  2641  reupick2  3467  dfiun2g  3973  iinss2  3994  invdisj  4052  mpteq12f  4140  trss  4167  sowlin  4385  reusv1  4523  reusv3  4525  ralxfrALT  4532  funimaexglem  5376  fun11iun  5565  fvmptssdm  5687  ffnfv  5761  riota5f  5947  mpoeq123  6027  tfri3  6476  nneneq  6979  mkvprop  7286  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  caucvgprlemm  7816  suplocexprlemss  7863  suplocsrlem  7956  indstr  9749  nninfinf  10625  prodeq2  11983  fprodle  12066  bezoutlemzz  12438  sgrpidmndm  13367  srgdilem  13846  ringdilem  13889  tgcl  14651  fsumcncntop  15154  dedekindeulemlu  15208  dedekindicclemlu  15217  bj-rspgt  15922  bj-charfunr  15945