Theorem rspsbc

Description: Restricted quantifier version of Axiom 4 of Mendelson p. 69. This provides an axiom for a predicate calculus for a restricted domain. This theorem generalizes the unrestricted stdpc4 and spsbc . See also rspsbca and rspcsbela . (Contributed by NM, 17-Nov-2006) (Proof shortened by Mario Carneiro, 13-Oct-2016)

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

Proof

Step	Hyp	Ref	Expression
1		cbvralsvw	|- ( A. x e. B ph <-> A. y e. B [ y / x ] ph )
2		dfsbcq2	|- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )
3	2	rspcv	|- ( A e. B -> ( A. y e. B [ y / x ] ph -> [. A / x ]. ph ) )
4	1 3	syl5bi	|- ( A e. B -> ( A. x e. B ph -> [. A / x ]. ph ) )