Theorem rspec 3251

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

Syntax hints:   → wi 4   ∈ wcel 2103  ∀wral 3063

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 2173

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

This theorem is referenced by:  rspec2  3280  vtoclri  3599  wfis  6386  wfis2f  6389  wfis2  6391  isarep2  6668  mpoexw  8115  ecopover  8875  frins  9817  alephsuc2  10145  indstr  12977  reltxrnmnf  13400  ackbijnn  15872  mrelatglb0  18626  0frgp  19816  iccpnfcnv  24987  prter2  38785  natlocalincr  46729  natglobalincr  46730