Theorem rspec 3223

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∀wral 3047

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 2180

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

This theorem is referenced by:  rspec2  3251  vtoclri  3540  wfis  6299  wfis2f  6301  wfis2  6303  isarep2  6571  mpoexw  8010  ecopover  8745  frins  9645  alephsuc2  9971  indstr  12814  reltxrnmnf  13242  ackbijnn  15735  mrelatglb0  18467  0frgp  19691  iccpnfcnv  24869  prter2  38990  natlocalincr  46984  natglobalincr  46985