Theorem rspec 3255

Description: Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994.)

Hypothesis

Ref	Expression
rspec.1	⊢ ∀𝑥 ∈ 𝐴 𝜑

Assertion

Ref	Expression
rspec	⊢ (𝑥 ∈ 𝐴 → 𝜑)

Proof of Theorem rspec

Step	Hyp	Ref	Expression
1		rspec.1	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝜑
2		rsp 3252	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (𝑥 ∈ 𝐴 → 𝜑)

Syntax hints:   → wi 4   ∈ wcel 2144  ∀wral 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-12 2214

This theorem depends on definitions:  df-bi 209  df-ex 1802  df-ral 3079

This theorem is referenced by:  rspec2  3283  vtoclri  3551  rab0  4341  wfis  6341  wfis2f  6343  wfis2  6345  isarep2  6613  mpoexw  8061  ecopover  8805  frins  9712  alephsuc2  10038  indstr  12919  reltxrnmnf  13348  ackbijnn  15860  mrelatglb0  18595  0frgp  19821  iccpnfcnv  25008  prter2  39510  natlocalincr  47457  natglobalincr  47458