Theorem rspec 3256

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2143  ∀wral 3079

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-12 2213

This proof depends on definitions:  df-bi 210  df-ex 1810  df-ral 3080

This theorem is used by:  rspec2  3284  vtoclri  3549  rab0  4342  wfis  6353  wfis2f  6355  wfis2  6357  isarep2  6625  mpoexw  8071  ecopover  8815  frins  9720  alephsuc2  10069  indstr  12944  reltxrnmnf  13373  ackbijnn  15887  mrelatglb0  18621  0frgp  19853  iccpnfcnv  25112  prter2  39683  natlocalincr  47620  natglobalincr  47621