Theorem rspec 3225

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

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

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 2182

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

This theorem is referenced by:  rspec2  3253  vtoclri  3542  wfis  6308  wfis2f  6310  wfis2  6312  isarep2  6580  mpoexw  8020  ecopover  8756  frins  9662  alephsuc2  9988  indstr  12827  reltxrnmnf  13256  ackbijnn  15749  mrelatglb0  18482  0frgp  19706  iccpnfcnv  24896  prter2  39080  natlocalincr  47062  natglobalincr  47063