This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbccom

Description: Commutative law for double class substitution. (Contributed by NM, 15-Nov-2005) (Proof shortened by Mario Carneiro, 18-Oct-2016)

Ref Expression
Assertion sbccom ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )

Proof

Step Hyp Ref Expression
1 sbccomlem ⊢ ( [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝐵 / 𝑤 ] [ 𝐴 / 𝑧 ] [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 )
2 sbccomlem ⊢ ( [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
3 2 sbcbii ⊢ ( [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝐵 / 𝑤 ] [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
4 sbccomlem ⊢ ( [ 𝐵 / 𝑤 ] [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 )
5 3 4 bitri ⊢ ( [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 )
6 5 sbcbii ⊢ ( [ 𝐴 / 𝑧 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 )
7 sbccomlem ⊢ ( [ 𝐴 / 𝑧 ] [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑤 / 𝑦 ] [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] 𝜑 )
8 7 sbcbii ⊢ ( [ 𝐵 / 𝑤 ] [ 𝐴 / 𝑧 ] [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] 𝜑 )
9 1 6 8 3bitr3i ⊢ ( [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] 𝜑 )
10 sbccow ⊢ ( [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 )
11 sbccow ⊢ ( [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] 𝜑 )
12 9 10 11 3bitr3i ⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] 𝜑 )
13 sbccow ⊢ ( [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] 𝜑 )
14 13 sbcbii ⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 )
15 sbccow ⊢ ( [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 )
16 15 sbcbii ⊢ ( [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )
17 12 14 16 3bitr3i ⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )