Theorem sbccom2lem

Description: Lemma for sbccom2 . (Contributed by Giovanni Mascellani, 31-May-2019)

	Ref	Expression
Hypothesis	sbccom2lem.1	$$⊢A\in \mathrm{V}$$
Assertion	sbccom2lem	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$

Proof

Step	Hyp	Ref	Expression
1		sbccom2lem.1	$$⊢A\in \mathrm{V}$$
2		sbcan	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y=B\wedge \phi \right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
3		sbc5	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(y=B\wedge \phi \right)\leftrightarrow \exists x\left(x=A\wedge \left(y=B\wedge \phi \right)\right)$$
4	1	csbconstgi	$$⊢⦋A/x⦌y=y$$
5		eqid	$$⊢⦋A/x⦌B=⦋A/x⦌B$$
6	1 4 5	sbceqi	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\leftrightarrow y=⦋A/x⦌B$$
7	6	anbi1i	$$⊢\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y=B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(y=⦋A/x⦌B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
8	2 3 7	3bitr3i	$$⊢\exists x\left(x=A\wedge \left(y=B\wedge \phi \right)\right)\leftrightarrow \left(y=⦋A/x⦌B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
9	8	exbii	$$⊢\exists y\exists x\left(x=A\wedge \left(y=B\wedge \phi \right)\right)\leftrightarrow \exists y\left(y=⦋A/x⦌B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
10		sbc5	$$⊢\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \exists y\left(y=B\wedge \phi \right)$$
11	10	sbcbii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(y=B\wedge \phi \right)$$
12		sbc5	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\exists y\left(y=B\wedge \phi \right)\leftrightarrow \exists x\left(x=A\wedge \exists y\left(y=B\wedge \phi \right)\right)$$
13	11 12	bitri	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \exists x\left(x=A\wedge \exists y\left(y=B\wedge \phi \right)\right)$$
14		19.42v	$$⊢\exists y\left(x=A\wedge \left(y=B\wedge \phi \right)\right)\leftrightarrow \left(x=A\wedge \exists y\left(y=B\wedge \phi \right)\right)$$
15	14	bicomi	$$⊢\left(x=A\wedge \exists y\left(y=B\wedge \phi \right)\right)\leftrightarrow \exists y\left(x=A\wedge \left(y=B\wedge \phi \right)\right)$$
16	15	exbii	$$⊢\exists x\left(x=A\wedge \exists y\left(y=B\wedge \phi \right)\right)\leftrightarrow \exists x\exists y\left(x=A\wedge \left(y=B\wedge \phi \right)\right)$$
17		excom	$$⊢\exists x\exists y\left(x=A\wedge \left(y=B\wedge \phi \right)\right)\leftrightarrow \exists y\exists x\left(x=A\wedge \left(y=B\wedge \phi \right)\right)$$
18	16 17	bitri	$$⊢\exists x\left(x=A\wedge \exists y\left(y=B\wedge \phi \right)\right)\leftrightarrow \exists y\exists x\left(x=A\wedge \left(y=B\wedge \phi \right)\right)$$
19	13 18	bitri	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \exists y\exists x\left(x=A\wedge \left(y=B\wedge \phi \right)\right)$$
20		sbc5	$$⊢\underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \exists y\left(y=⦋A/x⦌B\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
21	9 19 20	3bitr4i	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$