Theorem rsp 2411

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1282   ∈ wcel 1433  ∀wral 2348

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

This theorem depends on definitions:  df-bi 115  df-ral 2353

This theorem is referenced by:  rsp2  2413  rspec  2415  r19.12  2466  ralbi  2489  rexbi  2490  reupick2  3250  dfiun2g  3710  iinss2  3730  invdisj  3780  mpteq12f  3858  trss  3884  sowlin  4075  reusv1  4208  reusv3  4210  ralxfrALT  4217  funimaexglem  5002  fun11iun  5167  fvmptssdm  5276  ffnfv  5344  riota5f  5512  mpt2eq123  5584  tfri3  5976  nneneq  6343  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  caucvgprlemm  6858  indstr  8681  bezoutlemzz  10391  bj-rspgt  10596