Metamath Proof Explorer


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 B x B φ [˙A / x]˙ φ

Proof

Step Hyp Ref Expression
1 cbvralsvw x B φ y B y x φ
2 dfsbcq2 y = A y x φ [˙A / x]˙ φ
3 2 rspcv A B y B y x φ [˙A / x]˙ φ
4 1 3 syl5bi A B x B φ [˙A / x]˙ φ