Theorem rsp 2513

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1341   ∈ wcel 2136  ∀wral 2444

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

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

This theorem is referenced by:  rspa  2514  rsp2  2516  rspec  2518  r19.12  2572  ralbi  2598  rexbi  2599  reupick2  3408  dfiun2g  3898  iinss2  3918  invdisj  3976  mpteq12f  4062  trss  4089  sowlin  4298  reusv1  4436  reusv3  4438  ralxfrALT  4445  funimaexglem  5271  fun11iun  5453  fvmptssdm  5570  ffnfv  5643  riota5f  5822  mpoeq123  5901  tfri3  6335  nneneq  6823  mkvprop  7122  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  caucvgprlemm  7609  suplocexprlemss  7656  suplocsrlem  7749  indstr  9531  prodeq2  11498  fprodle  11581  bezoutlemzz  11935  tgcl  12704  fsumcncntop  13196  dedekindeulemlu  13239  dedekindicclemlu  13248  bj-rspgt  13667  bj-charfunr  13692