Theorem rspec 3220

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-ral 3045

This theorem is referenced by:  rspec2  3248  vtoclri  3545  wfis  6300  wfis2f  6302  wfis2  6304  isarep2  6572  mpoexw  8013  ecopover  8748  frins  9648  alephsuc2  9974  indstr  12817  reltxrnmnf  13245  ackbijnn  15735  mrelatglb0  18467  0frgp  19658  iccpnfcnv  24840  prter2  38870  natlocalincr  46867  natglobalincr  46868