Metamath Proof Explorer

Theorem sbccom2

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

Ref Expression
Hypothesis sbccom2.1 
|- A e. _V
Assertion sbccom2 
|- ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph )

Proof

Step Hyp Ref Expression
1 sbccom2.1 
 |-  A e. _V
2 sbcco 
 |-  ( [. B / w ]. [. w / y ]. ph <-> [. B / y ]. ph )
3 2 bicomi 
 |-  ( [. B / y ]. ph <-> [. B / w ]. [. w / y ]. ph )
4 3 sbcbii 
 |-  ( [. A / x ]. [. B / y ]. ph <-> [. A / x ]. [. B / w ]. [. w / y ]. ph )
5 sbcco 
 |-  ( [. A / z ]. [. z / x ]. [. B / w ]. [. w / y ]. ph <-> [. A / x ]. [. B / w ]. [. w / y ]. ph )
6 5 bicomi 
 |-  ( [. A / x ]. [. B / w ]. [. w / y ]. ph <-> [. A / z ]. [. z / x ]. [. B / w ]. [. w / y ]. ph )
7 vex 
 |-  z e. _V
8 7 sbccom2lem 
 |-  ( [. z / x ]. [. B / w ]. [. w / y ]. ph <-> [. [_ z / x ]_ B / w ]. [. z / x ]. [. w / y ]. ph )
9 8 sbcbii 
 |-  ( [. A / z ]. [. z / x ]. [. B / w ]. [. w / y ]. ph <-> [. A / z ]. [. [_ z / x ]_ B / w ]. [. z / x ]. [. w / y ]. ph )
10 4 6 9 3bitri 
 |-  ( [. A / x ]. [. B / y ]. ph <-> [. A / z ]. [. [_ z / x ]_ B / w ]. [. z / x ]. [. w / y ]. ph )
11 1 sbccom2lem 
 |-  ( [. A / z ]. [. [_ z / x ]_ B / w ]. [. z / x ]. [. w / y ]. ph <-> [. [_ A / z ]_ [_ z / x ]_ B / w ]. [. A / z ]. [. z / x ]. [. w / y ]. ph )
12 sbcco 
 |-  ( [. A / z ]. [. z / x ]. [. w / y ]. ph <-> [. A / x ]. [. w / y ]. ph )
13 12 sbcbii 
 |-  ( [. [_ A / z ]_ [_ z / x ]_ B / w ]. [. A / z ]. [. z / x ]. [. w / y ]. ph <-> [. [_ A / z ]_ [_ z / x ]_ B / w ]. [. A / x ]. [. w / y ]. ph )
14 10 11 13 3bitri 
 |-  ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / z ]_ [_ z / x ]_ B / w ]. [. A / x ]. [. w / y ]. ph )
15 csbco 
 |-  [_ A / z ]_ [_ z / x ]_ B = [_ A / x ]_ B
16 dfsbcq 
 |-  ( [_ A / z ]_ [_ z / x ]_ B = [_ A / x ]_ B -> ( [. [_ A / z ]_ [_ z / x ]_ B / w ]. [. A / x ]. [. w / y ]. ph <-> [. [_ A / x ]_ B / w ]. [. A / x ]. [. w / y ]. ph ) )
17 15 16 ax-mp 
 |-  ( [. [_ A / z ]_ [_ z / x ]_ B / w ]. [. A / x ]. [. w / y ]. ph <-> [. [_ A / x ]_ B / w ]. [. A / x ]. [. w / y ]. ph )
18 14 17 bitri 
 |-  ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / w ]. [. A / x ]. [. w / y ]. ph )
19 sbccom 
 |-  ( [. A / x ]. [. w / y ]. ph <-> [. w / y ]. [. A / x ]. ph )
20 19 sbcbii 
 |-  ( [. [_ A / x ]_ B / w ]. [. A / x ]. [. w / y ]. ph <-> [. [_ A / x ]_ B / w ]. [. w / y ]. [. A / x ]. ph )
21 sbcco 
 |-  ( [. [_ A / x ]_ B / w ]. [. w / y ]. [. A / x ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph )
22 18 20 21 3bitri 
 |-  ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. [. A / x ]. ph )