Theorem rsp 2522

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 2458	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1509	. 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 1351   e. wcel 2146   A.wral 2453

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

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

This theorem is referenced by:  rspa  2523  rsp2  2525  rspec  2527  r19.12  2581  ralbi  2607  rexbi  2608  reupick2  3419  dfiun2g  3914  iinss2  3934  invdisj  3992  mpteq12f  4078  trss  4105  sowlin  4314  reusv1  4452  reusv3  4454  ralxfrALT  4461  funimaexglem  5291  fun11iun  5474  fvmptssdm  5592  ffnfv  5666  riota5f  5845  mpoeq123  5924  tfri3  6358  nneneq  6847  mkvprop  7146  cauappcvgprlemladdru  7630  cauappcvgprlemladdrl  7631  caucvgprlemm  7642  suplocexprlemss  7689  suplocsrlem  7782  indstr  9564  prodeq2  11531  fprodle  11614  bezoutlemzz  11968  sgrpidmndm  12685  srgdilem  12947  ringdilem  12990  tgcl  13133  fsumcncntop  13625  dedekindeulemlu  13668  dedekindicclemlu  13677  bj-rspgt  14096  bj-charfunr  14120