Metamath Proof Explorer

Theorem rspsbca

Description: Restricted quantifier version of Axiom 4 of Mendelson p. 69. (Contributed by NM, 14-Dec-2005)

Ref Expression
Assertion rspsbca 
|- ( ( A e. B /\ A. x e. B ph ) -> [. A / x ]. ph )

Proof

Step Hyp Ref Expression
1 rspsbc 
 |-  ( A e. B -> ( A. x e. B ph -> [. A / x ]. ph ) )
2 1 imp 
 |-  ( ( A e. B /\ A. x e. B ph ) -> [. A / x ]. ph )