Theorem rsp 2423

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

Assertion

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

Proof of Theorem rsp

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

Syntax hints:   → wi 4  ∀wal 1287   ∈ wcel 1438  ∀wral 2359

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

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

This theorem is referenced by:  rsp2  2425  rspec  2427  r19.12  2478  ralbi  2501  rexbi  2502  reupick2  3285  dfiun2g  3762  iinss2  3782  invdisj  3839  mpteq12f  3918  trss  3945  sowlin  4147  reusv1  4280  reusv3  4282  ralxfrALT  4289  funimaexglem  5097  fun11iun  5274  fvmptssdm  5387  ffnfv  5456  riota5f  5632  mpt2eq123  5708  tfri3  6132  nneneq  6573  cauappcvgprlemladdru  7215  cauappcvgprlemladdrl  7216  caucvgprlemm  7227  indstr  9081  bezoutlemzz  11269  bj-rspgt  11686