Theorem rspec 3253

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1813  df-ral 3077

This theorem is used by:  rspec2  3281  vtoclri  3544  rab0  4335  wfis  6352  wfis2f  6354  wfis2  6356  isarep2  6625  mpoexw  8082  ecopover  8828  frins  9741  alephsuc2  10108  indstr  12990  reltxrnmnf  13420  ackbijnn  15942  mrelatglb0  18674  0frgp  19932  iccpnfcnv  25204  prter2  39819