Theorem rspec 3262

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

Syntax hints:   → wi 4   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-ral 3086

This theorem is referenced by:  rspec2  3290  vtoclri  3558  rab0  4349  wfis  6354  wfis2f  6356  wfis2  6358  isarep2  6626  mpoexw  8075  ecopover  8819  frins  9724  alephsuc2  10064  indstr  12940  reltxrnmnf  13369  ackbijnn  15882  mrelatglb0  18617  0frgp  19849  iccpnfcnv  25072  prter2  39579  natlocalincr  47518  natglobalincr  47519