Theorem rspec 3257

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-12 2216

This proof depends on definitions:  df-bi 210  df-ex 1813  df-ral 3081

This theorem is used by:  rspec2  3285  vtoclri  3548  rab0  4338  wfis  6370  wfis2f  6372  wfis2  6374  isarep2  6648  mpoexw  8113  ecopover  8867  frins  9780  alephsuc2  10183  indstr  13067  reltxrnmnf  13497  ackbijnn  16023  mrelatglb0  18761  0frgp  20020  iccpnfcnv  25292  prter2  40129