Theorem csbcom2fi

Description: Commutative law for double class substitution in a class, with nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 4-Jun-2019)

	Ref	Expression
Hypotheses	csbcom2fi.1	|- A e. _V
	csbcom2fi.2	|- F/_ y A
	csbcom2fi.3	|- [_ A / x ]_ B = C
	csbcom2fi.4	|- [_ A / x ]_ D = E
Assertion	csbcom2fi	|- [_ A / x ]_ [_ B / y ]_ D = [_ C / y ]_ E

Proof

Step	Hyp	Ref	Expression
1		csbcom2fi.1	|- A e. _V
2		csbcom2fi.2	|- F/_ y A
3		csbcom2fi.3	|- [_ A / x ]_ B = C
4		csbcom2fi.4	|- [_ A / x ]_ D = E
5		df-csb	|- [_ A / x ]_ [_ B / y ]_ D = { z | [. A / x ]. z e. [_ B / y ]_ D }
6	5	abeq2i	|- ( z e. [_ A / x ]_ [_ B / y ]_ D <-> [. A / x ]. z e. [_ B / y ]_ D )
7		df-csb	|- [_ B / y ]_ D = { z | [. B / y ]. z e. D }
8	7	abeq2i	|- ( z e. [_ B / y ]_ D <-> [. B / y ]. z e. D )
9	8	sbcbii	|- ( [. A / x ]. z e. [_ B / y ]_ D <-> [. A / x ]. [. B / y ]. z e. D )
10	6 9	bitri	|- ( z e. [_ A / x ]_ [_ B / y ]_ D <-> [. A / x ]. [. B / y ]. z e. D )
11		df-csb	|- [_ A / x ]_ D = { z | [. A / x ]. z e. D }
12	11	abeq2i	|- ( z e. [_ A / x ]_ D <-> [. A / x ]. z e. D )
13	4	eleq2i	|- ( z e. [_ A / x ]_ D <-> z e. E )
14	12 13	bitr3i	|- ( [. A / x ]. z e. D <-> z e. E )
15	1 2 3 14	sbccom2fi	|- ( [. A / x ]. [. B / y ]. z e. D <-> [. C / y ]. z e. E )
16		sbcel2	|- ( [. C / y ]. z e. E <-> z e. [_ C / y ]_ E )
17	10 15 16	3bitri	|- ( z e. [_ A / x ]_ [_ B / y ]_ D <-> z e. [_ C / y ]_ E )
18	17	eqriv	|- [_ A / x ]_ [_ B / y ]_ D = [_ C / y ]_ E