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 ⊢ [˙A / x]˙ [˙B / y]˙ φ ↔ [˙B / y]˙ [˙A / x]˙ φ

Proof

Step Hyp Ref Expression
1 sbccomlem ⊢ [˙A / z]˙ [˙B / w]˙ [˙w / y]˙ [˙z / x]˙ φ ↔ [˙B / w]˙ [˙A / z]˙ [˙w / y]˙ [˙z / x]˙ φ
2 sbccomlem ⊢ [˙w / y]˙ [˙z / x]˙ φ ↔ [˙z / x]˙ [˙w / y]˙ φ
3 2 sbcbii ⊢ [˙B / w]˙ [˙w / y]˙ [˙z / x]˙ φ ↔ [˙B / w]˙ [˙z / x]˙ [˙w / y]˙ φ
4 sbccomlem ⊢ [˙B / w]˙ [˙z / x]˙ [˙w / y]˙ φ ↔ [˙z / x]˙ [˙B / w]˙ [˙w / y]˙ φ
5 3 4 bitri ⊢ [˙B / w]˙ [˙w / y]˙ [˙z / x]˙ φ ↔ [˙z / x]˙ [˙B / w]˙ [˙w / y]˙ φ
6 5 sbcbii ⊢ [˙A / z]˙ [˙B / w]˙ [˙w / y]˙ [˙z / x]˙ φ ↔ [˙A / z]˙ [˙z / x]˙ [˙B / w]˙ [˙w / y]˙ φ
7 sbccomlem ⊢ [˙A / z]˙ [˙w / y]˙ [˙z / x]˙ φ ↔ [˙w / y]˙ [˙A / z]˙ [˙z / x]˙ φ
8 7 sbcbii ⊢ [˙B / w]˙ [˙A / z]˙ [˙w / y]˙ [˙z / x]˙ φ ↔ [˙B / w]˙ [˙w / y]˙ [˙A / z]˙ [˙z / x]˙ φ
9 1 6 8 3bitr3i ⊢ [˙A / z]˙ [˙z / x]˙ [˙B / w]˙ [˙w / y]˙ φ ↔ [˙B / w]˙ [˙w / y]˙ [˙A / z]˙ [˙z / x]˙ φ
10 sbccow ⊢ [˙A / z]˙ [˙z / x]˙ [˙B / w]˙ [˙w / y]˙ φ ↔ [˙A / x]˙ [˙B / w]˙ [˙w / y]˙ φ
11 sbccow ⊢ [˙B / w]˙ [˙w / y]˙ [˙A / z]˙ [˙z / x]˙ φ ↔ [˙B / y]˙ [˙A / z]˙ [˙z / x]˙ φ
12 9 10 11 3bitr3i ⊢ [˙A / x]˙ [˙B / w]˙ [˙w / y]˙ φ ↔ [˙B / y]˙ [˙A / z]˙ [˙z / x]˙ φ
13 sbccow ⊢ [˙B / w]˙ [˙w / y]˙ φ ↔ [˙B / y]˙ φ
14 13 sbcbii ⊢ [˙A / x]˙ [˙B / w]˙ [˙w / y]˙ φ ↔ [˙A / x]˙ [˙B / y]˙ φ
15 sbccow ⊢ [˙A / z]˙ [˙z / x]˙ φ ↔ [˙A / x]˙ φ
16 15 sbcbii ⊢ [˙B / y]˙ [˙A / z]˙ [˙z / x]˙ φ ↔ [˙B / y]˙ [˙A / x]˙ φ
17 12 14 16 3bitr3i ⊢ [˙A / x]˙ [˙B / y]˙ φ ↔ [˙B / y]˙ [˙A / x]˙ φ