Theorem rspec 3248

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∀wral 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-12 2175

This theorem depends on definitions:  df-bi 207  df-ex 1777  df-ral 3060

This theorem is referenced by:  rspec2  3277  vtoclri  3590  wfis  6378  wfis2f  6381  wfis2  6383  isarep2  6659  mpoexw  8102  ecopover  8860  frins  9790  alephsuc2  10118  indstr  12956  reltxrnmnf  13381  ackbijnn  15861  mrelatglb0  18619  0frgp  19812  iccpnfcnv  24989  prter2  38863  natlocalincr  46830  natglobalincr  46831