Theorem rsp 2544

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 2480	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		sp 1525	. 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 2167   A.wral 2475

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

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

This theorem is referenced by:  rspa  2545  rsp2  2547  rspec  2549  r19.12  2603  ralbi  2629  rexbi  2630  reupick2  3450  dfiun2g  3949  iinss2  3970  invdisj  4028  mpteq12f  4114  trss  4141  sowlin  4356  reusv1  4494  reusv3  4496  ralxfrALT  4503  funimaexglem  5342  fun11iun  5528  fvmptssdm  5649  ffnfv  5723  riota5f  5905  mpoeq123  5985  tfri3  6434  nneneq  6927  mkvprop  7233  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  caucvgprlemm  7752  suplocexprlemss  7799  suplocsrlem  7892  indstr  9684  nninfinf  10552  prodeq2  11739  fprodle  11822  bezoutlemzz  12194  sgrpidmndm  13122  srgdilem  13601  ringdilem  13644  tgcl  14384  fsumcncntop  14887  dedekindeulemlu  14941  dedekindicclemlu  14950  bj-rspgt  15516  bj-charfunr  15540