Theorem rsp 2580

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 2516	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1560	. 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 1396   e. wcel 2202   A.wral 2511

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

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

This theorem is referenced by:  rspa  2581  rsp2  2583  rspec  2585  r19.12  2640  ralbi  2666  rexbi  2667  reupick2  3495  dfiun2g  4007  iinss2  4028  invdisj  4086  mpteq12f  4174  trss  4201  sowlin  4423  reusv1  4561  reusv3  4563  ralxfrALT  4570  funimaexglem  5420  fun11iun  5613  fvmptssdm  5740  ffnfv  5813  riota5f  6008  mpoeq123  6090  tfri3  6576  nneneq  7086  mkvprop  7417  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  caucvgprlemm  7948  suplocexprlemss  7995  suplocsrlem  8088  indstr  9888  nninfinf  10768  prodeq2  12198  fprodle  12281  bezoutlemzz  12653  sgrpidmndm  13583  srgdilem  14063  ringdilem  14106  tgcl  14875  fsumcncntop  15378  dedekindeulemlu  15432  dedekindicclemlu  15441  bj-rspgt  16504  bj-charfunr  16526