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\in B\to \left(\forall x\in B\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		cbvralsvw	$$⊢\forall x\in B\phi \leftrightarrow \forall y\in B\left[y/x\right]\phi$$
2		dfsbcq2	$$⊢y=A\to \left(\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
3	2	rspcv	$$⊢A\in B\to \left(\forall y\in B\left[y/x\right]\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
4	1 3	syl5bi	$$⊢A\in B\to \left(\forall x\in B\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$