Theorem rspec 3237

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-12 2176

This theorem depends on definitions:  df-bi 207  df-ex 1779  df-ral 3051

This theorem is referenced by:  rspec2  3265  vtoclri  3574  wfis  6357  wfis2f  6360  wfis2  6362  isarep2  6639  mpoexw  8086  ecopover  8844  frins  9775  alephsuc2  10103  indstr  12941  reltxrnmnf  13367  ackbijnn  15847  mrelatglb0  18580  0frgp  19770  iccpnfcnv  24930  prter2  38823  natlocalincr  46836  natglobalincr  46837