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 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

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

This theorem is used by:  rspec2  3281  vtoclri  3544  rab0  4334  wfis  6355  wfis2f  6357  wfis2  6359  isarep2  6629  mpoexw  8091  ecopover  8842  frins  9756  alephsuc2  10159  indstr  13043  reltxrnmnf  13473  ackbijnn  15997  mrelatglb0  18735  0frgp  19993  iccpnfcnv  25265  prter2  39939