Metamath Proof Explorer

Theorem rspa

Description: Restricted specialization. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion rspa 
|- ( ( A. x e. A ph /\ x e. A ) -> ph )

Proof

Step Hyp Ref Expression
1 rsp 
 |-  ( A. x e. A ph -> ( x e. A -> ph ) )
2 1 imp 
 |-  ( ( A. x e. A ph /\ x e. A ) -> ph )