Theorem rspec 3230

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

Syntax hints:   → wi 4   ∈ wcel 2119  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-12 2189

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-ral 3054

This theorem is referenced by:  rspec2  3258  vtoclri  3528  wfis  6304  wfis2f  6306  wfis2  6308  isarep2  6576  mpoexw  8021  ecopover  8759  frins  9668  alephsuc2  9994  indstr  12858  reltxrnmnf  13287  ackbijnn  15785  mrelatglb0  18519  0frgp  19746  iccpnfcnv  24930  prter2  39382  natlocalincr  47329  natglobalincr  47330