Theorem sbcnestgfw

Description: Nest the composition of two substitutions. Version of sbcnestgf with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 11-Nov-2016) (Revised by Gino Giotto, 26-Jan-2024)

	Ref	Expression
Assertion	sbcnestgfw	$$⊢\left(A\in V\wedge \forall yℲx\phi \right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		dfsbcq	$$⊢z=A\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \right)$$
2		csbeq1	$$⊢z=A\to ⦋z/x⦌B=⦋A/x⦌B$$
3	2	sbceq1d	$$⊢z=A\to \left(\underset{\dot{}}{[}⦋z/x⦌B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\phi \right)$$
4	1 3	bibi12d	$$⊢z=A\to \left(\left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋z/x⦌B/y\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\phi \right)\right)$$
5	4	imbi2d	$$⊢z=A\to \left(\left(\forall yℲx\phi \to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋z/x⦌B/y\underset{\dot{}}{]}\phi \right)\right)\leftrightarrow \left(\forall yℲx\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\phi \right)\right)\right)$$
6		vex	$$⊢z\in \mathrm{V}$$
7	6	a1i	$$⊢\forall yℲx\phi \to z\in \mathrm{V}$$
8		csbeq1a	$$⊢x=z\to B=⦋z/x⦌B$$
9	8	sbceq1d	$$⊢x=z\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋z/x⦌B/y\underset{\dot{}}{]}\phi \right)$$
10	9	adantl	$$⊢\left(\forall yℲx\phi \wedge x=z\right)\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋z/x⦌B/y\underset{\dot{}}{]}\phi \right)$$
11		nfnf1	$$⊢ℲxℲx\phi$$
12	11	nfal	$$⊢Ⅎx\forall yℲx\phi$$
13		nfa1	$$⊢Ⅎy\forall yℲx\phi$$
14		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋z/x⦌B$$
15	14	a1i	$$⊢\forall yℲx\phi \to \underset{\_}{Ⅎ}x⦋z/x⦌B$$
16		sp	$$⊢\forall yℲx\phi \to Ⅎx\phi$$
17	13 15 16	nfsbcdw	$$⊢\forall yℲx\phi \to Ⅎx\underset{\dot{}}{[}⦋z/x⦌B/y\underset{\dot{}}{]}\phi$$
18	7 10 12 17	sbciedf	$$⊢\forall yℲx\phi \to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋z/x⦌B/y\underset{\dot{}}{]}\phi \right)$$
19	5 18	vtoclg	$$⊢A\in V\to \left(\forall yℲx\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\phi \right)\right)$$
20	19	imp	$$⊢\left(A\in V\wedge \forall yℲx\phi \right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\phi \right)$$