Theorem rsp 2537

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 2473	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1522	. 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 2160   A.wral 2468

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

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

This theorem is referenced by:  rspa  2538  rsp2  2540  rspec  2542  r19.12  2596  ralbi  2622  rexbi  2623  reupick2  3436  dfiun2g  3933  iinss2  3954  invdisj  4012  mpteq12f  4098  trss  4125  sowlin  4338  reusv1  4476  reusv3  4478  ralxfrALT  4485  funimaexglem  5318  fun11iun  5501  fvmptssdm  5620  ffnfv  5694  riota5f  5875  mpoeq123  5954  tfri3  6391  nneneq  6884  mkvprop  7185  cauappcvgprlemladdru  7684  cauappcvgprlemladdrl  7685  caucvgprlemm  7696  suplocexprlemss  7743  suplocsrlem  7836  indstr  9622  prodeq2  11596  fprodle  11679  bezoutlemzz  12034  sgrpidmndm  12878  srgdilem  13320  ringdilem  13363  tgcl  14016  fsumcncntop  14508  dedekindeulemlu  14551  dedekindicclemlu  14560  bj-rspgt  14991  bj-charfunr  15015