Theorem csbco3g

Description: Composition of two class substitutions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 27-Nov-2005) (Revised by Mario Carneiro, 11-Nov-2016) (New usage is discouraged.)

	Ref	Expression
Hypothesis	sbcco3g.1	$$⊢x=A\to B=C$$
Assertion	csbco3g	$$⊢A\in V\to ⦋A/x⦌⦋B/y⦌D=⦋C/y⦌D$$

Proof

Step	Hyp	Ref	Expression
1		sbcco3g.1	$$⊢x=A\to B=C$$
2		csbnestg	$$⊢A\in V\to ⦋A/x⦌⦋B/y⦌D=⦋⦋A/x⦌B/y⦌D$$
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	3 5	syl	$$⊢A\in V\to ⦋A/x⦌B=C$$
7	6	csbeq1d	$$⊢A\in V\to ⦋⦋A/x⦌B/y⦌D=⦋C/y⦌D$$
8	2 7	eqtrd	$$⊢A\in V\to ⦋A/x⦌⦋B/y⦌D=⦋C/y⦌D$$