Theorem rspec 3256

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 3253	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → (𝑥 ∈ 𝐴 → 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (𝑥 ∈ 𝐴 → 𝜑)

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-ral 3068

This theorem is referenced by:  rspec2  3285  vtoclri  3603  wfis  6387  wfis2f  6390  wfis2  6392  isarep2  6669  mpoexw  8119  ecopover  8879  frins  9821  alephsuc2  10149  indstr  12981  reltxrnmnf  13404  ackbijnn  15876  mrelatglb0  18631  0frgp  19821  iccpnfcnv  24994  prter2  38837  natlocalincr  46795  natglobalincr  46796