Theorem rspec 3227

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

Syntax hints:   → wi 4   ∈ wcel 2113  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2184

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-ral 3052

This theorem is referenced by:  rspec2  3255  vtoclri  3544  wfis  6310  wfis2f  6312  wfis2  6314  isarep2  6582  mpoexw  8022  ecopover  8760  frins  9666  alephsuc2  9992  indstr  12831  reltxrnmnf  13260  ackbijnn  15753  mrelatglb0  18486  0frgp  19710  iccpnfcnv  24900  prter2  39163  natlocalincr  47141  natglobalincr  47142