Theorem sbc3ie

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Jun-2014) (Revised by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	sbc3ie.1	$$⊢A\in \mathrm{V}$$
	sbc3ie.2	$$⊢B\in \mathrm{V}$$
	sbc3ie.3	$$⊢C\in \mathrm{V}$$
	sbc3ie.4	$$⊢\left(x=A\wedge y=B\wedge z=C\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	sbc3ie	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\underset{\dot{}}{[}C/z\underset{\dot{}}{]}\phi \leftrightarrow \psi$$

Proof

Step	Hyp	Ref	Expression
1		sbc3ie.1	$$⊢A\in \mathrm{V}$$
2		sbc3ie.2	$$⊢B\in \mathrm{V}$$
3		sbc3ie.3	$$⊢C\in \mathrm{V}$$
4		sbc3ie.4	$$⊢\left(x=A\wedge y=B\wedge z=C\right)\to \left(\phi \leftrightarrow \psi \right)$$
5	3	a1i	$$⊢\left(x=A\wedge y=B\right)\to C\in \mathrm{V}$$
6	4	3expa	$$⊢\left(\left(x=A\wedge y=B\right)\wedge z=C\right)\to \left(\phi \leftrightarrow \psi \right)$$
7	5 6	sbcied	$$⊢\left(x=A\wedge y=B\right)\to \left(\underset{\dot{}}{[}C/z\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$
8	1 2 7	sbc2ie	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\underset{\dot{}}{[}C/z\underset{\dot{}}{]}\phi \leftrightarrow \psi$$