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

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 ⊢ ⦋ A / x⦌ ⦋ B / y⦌ C = ⦋ B / y⦌ ⦋ A / x⦌ C

Proof

Step Hyp Ref Expression
1 sbccom ⊢ [˙A / x]˙ [˙B / y]˙ z ∈ C ↔ [˙B / y]˙ [˙A / x]˙ z ∈ C
2 sbcel2 ⊢ [˙B / y]˙ z ∈ C ↔ z ∈ ⦋ B / y⦌ C
3 2 sbcbii ⊢ [˙A / x]˙ [˙B / y]˙ z ∈ C ↔ [˙A / x]˙ z ∈ ⦋ B / y⦌ C
4 sbcel2 ⊢ [˙A / x]˙ z ∈ C ↔ z ∈ ⦋ A / x⦌ C
5 4 sbcbii ⊢ [˙B / y]˙ [˙A / x]˙ z ∈ C ↔ [˙B / y]˙ z ∈ ⦋ A / x⦌ C
6 1 3 5 3bitr3i ⊢ [˙A / x]˙ z ∈ ⦋ B / y⦌ C ↔ [˙B / y]˙ z ∈ ⦋ A / x⦌ C
7 sbcel2 ⊢ [˙A / x]˙ z ∈ ⦋ B / y⦌ C ↔ z ∈ ⦋ A / x⦌ ⦋ B / y⦌ C
8 sbcel2 ⊢ [˙B / y]˙ z ∈ ⦋ A / x⦌ C ↔ z ∈ ⦋ B / y⦌ ⦋ A / x⦌ C
9 6 7 8 3bitr3i ⊢ z ∈ ⦋ A / x⦌ ⦋ B / y⦌ C ↔ z ∈ ⦋ B / y⦌ ⦋ A / x⦌ C
10 9 eqriv ⊢ ⦋ A / x⦌ ⦋ B / y⦌ C = ⦋ B / y⦌ ⦋ A / x⦌ C