Theorem sbcco3gw

Description: Composition of two substitutions. Version of sbcco3g with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 27-Nov-2005) Avoid ax-13 . (Revised by Gino Giotto, 26-Jan-2024)

	Ref	Expression
Hypothesis	sbcco3gw.1	$$⊢x=A\to B=C$$
Assertion	sbcco3gw	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}C/y\underset{\dot{}}{]}\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbcco3gw.1	$$⊢x=A\to B=C$$
2		sbcnestgw	$$⊢A\in V\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)$$
3		elex	$$⊢A\in V\to A\in \mathrm{V}$$
4		nfcvd	$$⊢A\in \mathrm{V}\to \underset{\_}{Ⅎ}xC$$
5	4 1	csbiegf	$$⊢A\in \mathrm{V}\to ⦋A/x⦌B=C$$
6		dfsbcq	$$⊢⦋A/x⦌B=C\to \left(\underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}C/y\underset{\dot{}}{]}\phi \right)$$
7	3 5 6	3syl	$$⊢A\in V\to \left(\underset{\dot{}}{[}⦋A/x⦌B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}C/y\underset{\dot{}}{]}\phi \right)$$
8	2 7	bitrd	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}C/y\underset{\dot{}}{]}\phi \right)$$