Theorem rsp 2524

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 2460	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1511	. 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 2148   A.wral 2455

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

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

This theorem is referenced by:  rspa  2525  rsp2  2527  rspec  2529  r19.12  2583  ralbi  2609  rexbi  2610  reupick2  3423  dfiun2g  3920  iinss2  3941  invdisj  3999  mpteq12f  4085  trss  4112  sowlin  4322  reusv1  4460  reusv3  4462  ralxfrALT  4469  funimaexglem  5301  fun11iun  5484  fvmptssdm  5602  ffnfv  5676  riota5f  5857  mpoeq123  5936  tfri3  6370  nneneq  6859  mkvprop  7158  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  caucvgprlemm  7669  suplocexprlemss  7716  suplocsrlem  7809  indstr  9595  prodeq2  11567  fprodle  11650  bezoutlemzz  12005  sgrpidmndm  12826  srgdilem  13157  ringdilem  13200  tgcl  13649  fsumcncntop  14141  dedekindeulemlu  14184  dedekindicclemlu  14193  bj-rspgt  14623  bj-charfunr  14647