Metamath Proof Explorer

Theorem csbcom

Description: Commutative law for double substitution into a class. (Contributed by NM, 14-Nov-2005) (Revised by NM, 18-Aug-2018)

Ref Expression
Assertion csbcom ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶

Proof

Step Hyp Ref Expression
1 sbccom ⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 ↔ [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐶 )
2 sbcel2 ⊢ ( [ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 ↔ 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 )
3 2 sbcbii ⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝑧 ∈ 𝐶 ↔ [ 𝐴 / 𝑥 ] 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 )
4 sbcel2 ⊢ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐶 ↔ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
5 4 sbcbii ⊢ ( [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐶 ↔ [ 𝐵 / 𝑦 ] 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
6 1 3 5 3bitr3i ⊢ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 ↔ [ 𝐵 / 𝑦 ] 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
7 sbcel2 ⊢ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 ↔ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 )
8 sbcel2 ⊢ ( [ 𝐵 / 𝑦 ] 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ↔ 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
9 6 7 8 3bitr3i ⊢ ( 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 ↔ 𝑧 ∈ ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )
10 9 eqriv ⊢ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ 𝐶 = ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝐴 / 𝑥 ⦌ 𝐶