Theorem rsp 2504

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1333   ∈ wcel 2128  ∀wral 2435

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

This theorem depends on definitions:  df-bi 116  df-ral 2440

This theorem is referenced by:  rspa  2505  rsp2  2507  rspec  2509  r19.12  2563  ralbi  2589  rexbi  2590  reupick2  3393  dfiun2g  3881  iinss2  3901  invdisj  3959  mpteq12f  4044  trss  4071  sowlin  4279  reusv1  4416  reusv3  4418  ralxfrALT  4425  funimaexglem  5250  fun11iun  5432  fvmptssdm  5549  ffnfv  5622  riota5f  5798  mpoeq123  5874  tfri3  6308  nneneq  6795  mkvprop  7084  cauappcvgprlemladdru  7559  cauappcvgprlemladdrl  7560  caucvgprlemm  7571  suplocexprlemss  7618  suplocsrlem  7711  indstr  9487  prodeq2  11436  fprodle  11519  bezoutlemzz  11866  tgcl  12424  fsumcncntop  12916  dedekindeulemlu  12959  dedekindicclemlu  12968  bj-rspgt  13319  bj-charfunr  13344