Theorem rsp 2369

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1241   ∈ wcel 1393  ∀wral 2306

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

This theorem depends on definitions:  df-bi 110  df-ral 2311

This theorem is referenced by:  rsp2  2371  rspec  2373  r19.12  2422  ralbi  2445  rexbi  2446  reupick2  3223  dfiun2g  3689  iinss2  3709  invdisj  3759  mpteq12f  3837  trss  3863  sowlin  4057  reusv1  4190  reusv3  4192  ralxfrALT  4199  funimaexglem  4982  fun11iun  5147  fvmptssdm  5255  ffnfv  5323  riota5f  5492  mpt2eq123  5564  tfri3  5953  nneneq  6320  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprlemm  6766  indstr  8536  bj-rspgt  9925