Theorem rsp 2597

Description: Restricted specialization. (Contributed by NM, 17-Oct-1996.)

Assertion

Ref	Expression
rsp	⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑))

Proof of Theorem rsp

Step	Hyp	Ref	Expression
1		df-ral 2533	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		sp 1564	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐴 → 𝜑))
3	1, 2	sylbi 121	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑))

This proof depends on syntax axioms:   → wi 4  ∀wal 1400   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-4 1563

This proof depends on definitions:  df-bi 117  df-ral 2533

This theorem is used by:  rspa  2598  rsp2  2600  rspec  2602  r19.12  2657  ralbi  2683  rexbi  2684  reupick2  3519  dfiun2g  4044  iinss2  4065  invdisj  4123  mpteq12f  4211  trss  4238  sowlin  4465  reusv1  4604  reusv3  4606  ralxfrALT  4613  funimaexglem  5464  fun11iun  5660  fvmptssdm  5790  ffnfv  5866  riota5f  6065  mpoeq123  6147  tfri3  6638  nneneq  7158  mkvprop  7499  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgprlemm  8036  suplocexprlemss  8083  suplocsrlem  8176  indstr  10003  nninfinf  10895  prodeq2  12343  fprodle  12426  bezoutlemzz  12798  sgrpidmndm  13786  srgdilem  14357  ringdilem  14400  tgcl  15256  fsumcncntop  15759  dedekindeulemlu  15813  dedekindicclemlu  15822  bj-rspgt  16980  bj-charfunr  17002