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 -> B = C )
Assertion	csbco3g	|- ( A e. V -> [_ A / x ]_ [_ B / y ]_ D = [_ C / y ]_ D )

Proof

Step	Hyp	Ref	Expression
1		sbcco3g.1	|- ( x = A -> B = C )
2		csbnestg	|- ( A e. V -> [_ A / x ]_ [_ B / y ]_ D = [_ [_ A / x ]_ B / y ]_ D )
3		elex	|- ( A e. V -> A e. _V )
4		nfcvd	|- ( A e. _V -> F/_ x C )
5	4 1	csbiegf	|- ( A e. _V -> [_ A / x ]_ B = C )
6	3 5	syl	|- ( A e. V -> [_ A / x ]_ B = C )
7	6	csbeq1d	|- ( A e. V -> [_ [_ A / x ]_ B / y ]_ D = [_ C / y ]_ D )
8	2 7	eqtrd	|- ( A e. V -> [_ A / x ]_ [_ B / y ]_ D = [_ C / y ]_ D )