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	⊢ 𝐴 ∈ V
	csbcom2fi.2	⊢ Ⅎ 𝑦 𝐴
	csbcom2fi.3	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶
	csbcom2fi.4	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 = 𝐸
Assertion	csbcom2fi	⊢ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐷 = ⦋ 𝐶 / 𝑦 ⦌ 𝐸

Proof

Step	Hyp	Ref	Expression
1		csbcom2fi.1	⊢ 𝐴 ∈ V
2		csbcom2fi.2	⊢ Ⅎ 𝑦 𝐴
3		csbcom2fi.3	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = 𝐶
4		csbcom2fi.4	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 = 𝐸
5		df-csb	⊢ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐷 = { 𝑧 ∣ [ 𝐴 / 𝑥 ] 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐷 }
6	5	abeq2i	⊢ ( 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐷 ↔ [ 𝐴 / 𝑥 ] 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐷 )
7		df-csb	⊢ ⦋ 𝐵 / 𝑦 ⦌ 𝐷 = { 𝑧 ∣ [ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐷 }
8	7	abeq2i	⊢ ( 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐷 ↔ [ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐷 )
9	8	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐷 ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐷 )
10	6 9	bitri	⊢ ( 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐷 ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐷 )
11		df-csb	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 = { 𝑧 ∣ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐷 }
12	11	abeq2i	⊢ ( 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ↔ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐷 )
13	4	eleq2i	⊢ ( 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ↔ 𝑧 ∈ 𝐸 )
14	12 13	bitr3i	⊢ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐷 ↔ 𝑧 ∈ 𝐸 )
15	1 2 3 14	sbccom2fi	⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐷 ↔ [ 𝐶 / 𝑦 ] 𝑧 ∈ 𝐸 )
16		sbcel2	⊢ ( [ 𝐶 / 𝑦 ] 𝑧 ∈ 𝐸 ↔ 𝑧 ∈ ⦋ 𝐶 / 𝑦 ⦌ 𝐸 )
17	10 15 16	3bitri	⊢ ( 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐷 ↔ 𝑧 ∈ ⦋ 𝐶 / 𝑦 ⦌ 𝐸 )
18	17	eqriv	⊢ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐷 = ⦋ 𝐶 / 𝑦 ⦌ 𝐸