Metamath Proof Explorer

Theorem sbccom2

Description: Commutative law for double class substitution. (Contributed by Giovanni Mascellani, 31-May-2019)

Ref Expression
Hypothesis sbccom2.1 ⊢ 𝐴 ∈ V
Assertion sbccom2 ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )

Proof

Step Hyp Ref Expression
1 sbccom2.1 ⊢ 𝐴 ∈ V
2 sbccow ⊢ ( [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] 𝜑 )
3 2 bicomi ⊢ ( [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 )
4 3 sbcbii ⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 )
5 sbccow ⊢ ( [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 )
6 5 bicomi ⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 )
7 vex ⊢ 𝑧 ∈ V
8 7 sbccom2lem ⊢ ( [ 𝑧 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 / 𝑤 ] [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
9 8 sbcbii ⊢ ( [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] [ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑧 ] [ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 / 𝑤 ] [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
10 4 6 9 3bitri ⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑧 ] [ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 / 𝑤 ] [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
11 1 sbccom2lem ⊢ ( [ 𝐴 / 𝑧 ] [ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 / 𝑤 ] [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑧 ⦌ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 / 𝑤 ] [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
12 sbccow ⊢ ( [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
13 12 sbcbii ⊢ ( [ ⦋ 𝐴 / 𝑧 ⦌ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 / 𝑤 ] [ 𝐴 / 𝑧 ] [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑧 ⦌ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 / 𝑤 ] [ 𝐴 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
14 10 11 13 3bitri ⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑧 ⦌ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 / 𝑤 ] [ 𝐴 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
15 csbcow ⊢ ⦋ 𝐴 / 𝑧 ⦌ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵
16 dfsbcq ⊢ ( ⦋ 𝐴 / 𝑧 ⦌ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵 → ( [ ⦋ 𝐴 / 𝑧 ⦌ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 / 𝑤 ] [ 𝐴 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑤 ] [ 𝐴 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) )
17 15 16 ax-mp ⊢ ( [ ⦋ 𝐴 / 𝑧 ⦌ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 / 𝑤 ] [ 𝐴 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑤 ] [ 𝐴 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
18 14 17 bitri ⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑤 ] [ 𝐴 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
19 sbccom ⊢ ( [ 𝐴 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑤 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )
20 19 sbcbii ⊢ ( [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑤 ] [ 𝐴 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )
21 sbccow ⊢ ( [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑤 ] [ 𝑤 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )
22 18 20 21 3bitri ⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )