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 e. C <-> [. B / y ]. [. A / x ]. z e. C )
2 sbcel2 
 |-  ( [. B / y ]. z e. C <-> z e. [_ B / y ]_ C )
3 2 sbcbii 
 |-  ( [. A / x ]. [. B / y ]. z e. C <-> [. A / x ]. z e. [_ B / y ]_ C )
4 sbcel2 
 |-  ( [. A / x ]. z e. C <-> z e. [_ A / x ]_ C )
5 4 sbcbii 
 |-  ( [. B / y ]. [. A / x ]. z e. C <-> [. B / y ]. z e. [_ A / x ]_ C )
6 1 3 5 3bitr3i 
 |-  ( [. A / x ]. z e. [_ B / y ]_ C <-> [. B / y ]. z e. [_ A / x ]_ C )
7 sbcel2 
 |-  ( [. A / x ]. z e. [_ B / y ]_ C <-> z e. [_ A / x ]_ [_ B / y ]_ C )
8 sbcel2 
 |-  ( [. B / y ]. z e. [_ A / x ]_ C <-> z e. [_ B / y ]_ [_ A / x ]_ C )
9 6 7 8 3bitr3i 
 |-  ( z e. [_ A / x ]_ [_ B / y ]_ C <-> z e. [_ B / y ]_ [_ A / x ]_ C )
10 9 eqriv 
 |-  [_ A / x ]_ [_ B / y ]_ C = [_ B / y ]_ [_ A / x ]_ C