Metamath Proof Explorer


Theorem rspec

Description: Specialization rule for restricted quantification. (Contributed by NM, 19-Nov-1994)

Ref Expression
Hypothesis rspec.1
|- A. x e. A ph
Assertion rspec
|- ( x e. A -> ph )

Proof

Step Hyp Ref Expression
1 rspec.1
 |-  A. x e. A ph
2 rsp
 |-  ( A. x e. A ph -> ( x e. A -> ph ) )
3 1 2 ax-mp
 |-  ( x e. A -> ph )