# Metamath Proof Explorer

## Theorem setscom

Description: Component-setting is commutative when the x-values are different. (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses setscom.1 ${⊢}{A}\in \mathrm{V}$
setscom.2 ${⊢}{B}\in \mathrm{V}$
Assertion setscom ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to \left({S}\mathrm{sSet}⟨{A},{C}⟩\right)\mathrm{sSet}⟨{B},{D}⟩=\left({S}\mathrm{sSet}⟨{B},{D}⟩\right)\mathrm{sSet}⟨{A},{C}⟩$

### Proof

Step Hyp Ref Expression
1 setscom.1 ${⊢}{A}\in \mathrm{V}$
2 setscom.2 ${⊢}{B}\in \mathrm{V}$
3 rescom ${⊢}{\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}={\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}$
4 3 uneq1i ${⊢}\left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}=\left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}$
5 4 uneq1i ${⊢}\left(\left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}\right)\cup \left\{⟨{B},{D}⟩\right\}=\left(\left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}\right)\cup \left\{⟨{B},{D}⟩\right\}$
6 un23 ${⊢}\left(\left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}\right)\cup \left\{⟨{B},{D}⟩\right\}=\left(\left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left\{⟨{B},{D}⟩\right\}\right)\cup \left\{⟨{A},{C}⟩\right\}$
7 5 6 eqtri ${⊢}\left(\left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}\right)\cup \left\{⟨{B},{D}⟩\right\}=\left(\left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left\{⟨{B},{D}⟩\right\}\right)\cup \left\{⟨{A},{C}⟩\right\}$
8 setsval ${⊢}\left({S}\in {V}\wedge {C}\in {W}\right)\to {S}\mathrm{sSet}⟨{A},{C}⟩=\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}$
9 8 ad2ant2r ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to {S}\mathrm{sSet}⟨{A},{C}⟩=\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}$
10 9 reseq1d ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to {\left({S}\mathrm{sSet}⟨{A},{C}⟩\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}={\left(\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}$
11 resundir ${⊢}{\left(\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}=\left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)\cup \left({\left\{⟨{A},{C}⟩\right\}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)$
12 elex ${⊢}{C}\in {W}\to {C}\in \mathrm{V}$
13 12 ad2antrl ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to {C}\in \mathrm{V}$
14 opelxpi ${⊢}\left({A}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)\to ⟨{A},{C}⟩\in \left(\mathrm{V}×\mathrm{V}\right)$
15 1 13 14 sylancr ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to ⟨{A},{C}⟩\in \left(\mathrm{V}×\mathrm{V}\right)$
16 opex ${⊢}⟨{A},{C}⟩\in \mathrm{V}$
17 16 relsn ${⊢}\mathrm{Rel}\left\{⟨{A},{C}⟩\right\}↔⟨{A},{C}⟩\in \left(\mathrm{V}×\mathrm{V}\right)$
18 15 17 sylibr ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to \mathrm{Rel}\left\{⟨{A},{C}⟩\right\}$
19 dmsnopss ${⊢}\mathrm{dom}\left\{⟨{A},{C}⟩\right\}\subseteq \left\{{A}\right\}$
20 disjsn2 ${⊢}{A}\ne {B}\to \left\{{A}\right\}\cap \left\{{B}\right\}=\varnothing$
21 20 ad2antlr ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to \left\{{A}\right\}\cap \left\{{B}\right\}=\varnothing$
22 disj2 ${⊢}\left\{{A}\right\}\cap \left\{{B}\right\}=\varnothing ↔\left\{{A}\right\}\subseteq \mathrm{V}\setminus \left\{{B}\right\}$
23 21 22 sylib ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to \left\{{A}\right\}\subseteq \mathrm{V}\setminus \left\{{B}\right\}$
24 19 23 sstrid ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to \mathrm{dom}\left\{⟨{A},{C}⟩\right\}\subseteq \mathrm{V}\setminus \left\{{B}\right\}$
25 relssres ${⊢}\left(\mathrm{Rel}\left\{⟨{A},{C}⟩\right\}\wedge \mathrm{dom}\left\{⟨{A},{C}⟩\right\}\subseteq \mathrm{V}\setminus \left\{{B}\right\}\right)\to {\left\{⟨{A},{C}⟩\right\}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}=\left\{⟨{A},{C}⟩\right\}$
26 18 24 25 syl2anc ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to {\left\{⟨{A},{C}⟩\right\}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}=\left\{⟨{A},{C}⟩\right\}$
27 26 uneq2d ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to \left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)\cup \left({\left\{⟨{A},{C}⟩\right\}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)=\left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}$
28 11 27 syl5eq ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to {\left(\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}=\left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}$
29 10 28 eqtrd ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to {\left({S}\mathrm{sSet}⟨{A},{C}⟩\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}=\left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}$
30 29 uneq1d ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to \left({\left({S}\mathrm{sSet}⟨{A},{C}⟩\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)\cup \left\{⟨{B},{D}⟩\right\}=\left(\left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}\right)\cup \left\{⟨{B},{D}⟩\right\}$
31 setsval ${⊢}\left({S}\in {V}\wedge {D}\in {X}\right)\to {S}\mathrm{sSet}⟨{B},{D}⟩=\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)\cup \left\{⟨{B},{D}⟩\right\}$
32 31 reseq1d ${⊢}\left({S}\in {V}\wedge {D}\in {X}\right)\to {\left({S}\mathrm{sSet}⟨{B},{D}⟩\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}={\left(\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)\cup \left\{⟨{B},{D}⟩\right\}\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}$
33 32 ad2ant2rl ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to {\left({S}\mathrm{sSet}⟨{B},{D}⟩\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}={\left(\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)\cup \left\{⟨{B},{D}⟩\right\}\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}$
34 resundir ${⊢}{\left(\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)\cup \left\{⟨{B},{D}⟩\right\}\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}=\left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left({\left\{⟨{B},{D}⟩\right\}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)$
35 elex ${⊢}{D}\in {X}\to {D}\in \mathrm{V}$
36 35 ad2antll ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to {D}\in \mathrm{V}$
37 opelxpi ${⊢}\left({B}\in \mathrm{V}\wedge {D}\in \mathrm{V}\right)\to ⟨{B},{D}⟩\in \left(\mathrm{V}×\mathrm{V}\right)$
38 2 36 37 sylancr ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to ⟨{B},{D}⟩\in \left(\mathrm{V}×\mathrm{V}\right)$
39 opex ${⊢}⟨{B},{D}⟩\in \mathrm{V}$
40 39 relsn ${⊢}\mathrm{Rel}\left\{⟨{B},{D}⟩\right\}↔⟨{B},{D}⟩\in \left(\mathrm{V}×\mathrm{V}\right)$
41 38 40 sylibr ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to \mathrm{Rel}\left\{⟨{B},{D}⟩\right\}$
42 dmsnopss ${⊢}\mathrm{dom}\left\{⟨{B},{D}⟩\right\}\subseteq \left\{{B}\right\}$
43 ssv ${⊢}\left\{{A}\right\}\subseteq \mathrm{V}$
44 ssv ${⊢}\left\{{B}\right\}\subseteq \mathrm{V}$
45 ssconb ${⊢}\left(\left\{{A}\right\}\subseteq \mathrm{V}\wedge \left\{{B}\right\}\subseteq \mathrm{V}\right)\to \left(\left\{{A}\right\}\subseteq \mathrm{V}\setminus \left\{{B}\right\}↔\left\{{B}\right\}\subseteq \mathrm{V}\setminus \left\{{A}\right\}\right)$
46 43 44 45 mp2an ${⊢}\left\{{A}\right\}\subseteq \mathrm{V}\setminus \left\{{B}\right\}↔\left\{{B}\right\}\subseteq \mathrm{V}\setminus \left\{{A}\right\}$
47 23 46 sylib ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to \left\{{B}\right\}\subseteq \mathrm{V}\setminus \left\{{A}\right\}$
48 42 47 sstrid ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to \mathrm{dom}\left\{⟨{B},{D}⟩\right\}\subseteq \mathrm{V}\setminus \left\{{A}\right\}$
49 relssres ${⊢}\left(\mathrm{Rel}\left\{⟨{B},{D}⟩\right\}\wedge \mathrm{dom}\left\{⟨{B},{D}⟩\right\}\subseteq \mathrm{V}\setminus \left\{{A}\right\}\right)\to {\left\{⟨{B},{D}⟩\right\}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}=\left\{⟨{B},{D}⟩\right\}$
50 41 48 49 syl2anc ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to {\left\{⟨{B},{D}⟩\right\}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}=\left\{⟨{B},{D}⟩\right\}$
51 50 uneq2d ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to \left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left({\left\{⟨{B},{D}⟩\right\}↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)=\left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left\{⟨{B},{D}⟩\right\}$
52 34 51 syl5eq ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to {\left(\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)\cup \left\{⟨{B},{D}⟩\right\}\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}=\left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left\{⟨{B},{D}⟩\right\}$
53 33 52 eqtrd ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to {\left({S}\mathrm{sSet}⟨{B},{D}⟩\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}=\left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left\{⟨{B},{D}⟩\right\}$
54 53 uneq1d ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to \left({\left({S}\mathrm{sSet}⟨{B},{D}⟩\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}=\left(\left({\left({{S}↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left\{⟨{B},{D}⟩\right\}\right)\cup \left\{⟨{A},{C}⟩\right\}$
55 7 30 54 3eqtr4a ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to \left({\left({S}\mathrm{sSet}⟨{A},{C}⟩\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)\cup \left\{⟨{B},{D}⟩\right\}=\left({\left({S}\mathrm{sSet}⟨{B},{D}⟩\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}$
56 ovex ${⊢}{S}\mathrm{sSet}⟨{A},{C}⟩\in \mathrm{V}$
57 simprr ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to {D}\in {X}$
58 setsval ${⊢}\left({S}\mathrm{sSet}⟨{A},{C}⟩\in \mathrm{V}\wedge {D}\in {X}\right)\to \left({S}\mathrm{sSet}⟨{A},{C}⟩\right)\mathrm{sSet}⟨{B},{D}⟩=\left({\left({S}\mathrm{sSet}⟨{A},{C}⟩\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)\cup \left\{⟨{B},{D}⟩\right\}$
59 56 57 58 sylancr ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to \left({S}\mathrm{sSet}⟨{A},{C}⟩\right)\mathrm{sSet}⟨{B},{D}⟩=\left({\left({S}\mathrm{sSet}⟨{A},{C}⟩\right)↾}_{\left(\mathrm{V}\setminus \left\{{B}\right\}\right)}\right)\cup \left\{⟨{B},{D}⟩\right\}$
60 ovex ${⊢}{S}\mathrm{sSet}⟨{B},{D}⟩\in \mathrm{V}$
61 simprl ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to {C}\in {W}$
62 setsval ${⊢}\left({S}\mathrm{sSet}⟨{B},{D}⟩\in \mathrm{V}\wedge {C}\in {W}\right)\to \left({S}\mathrm{sSet}⟨{B},{D}⟩\right)\mathrm{sSet}⟨{A},{C}⟩=\left({\left({S}\mathrm{sSet}⟨{B},{D}⟩\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}$
63 60 61 62 sylancr ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to \left({S}\mathrm{sSet}⟨{B},{D}⟩\right)\mathrm{sSet}⟨{A},{C}⟩=\left({\left({S}\mathrm{sSet}⟨{B},{D}⟩\right)↾}_{\left(\mathrm{V}\setminus \left\{{A}\right\}\right)}\right)\cup \left\{⟨{A},{C}⟩\right\}$
64 55 59 63 3eqtr4d ${⊢}\left(\left({S}\in {V}\wedge {A}\ne {B}\right)\wedge \left({C}\in {W}\wedge {D}\in {X}\right)\right)\to \left({S}\mathrm{sSet}⟨{A},{C}⟩\right)\mathrm{sSet}⟨{B},{D}⟩=\left({S}\mathrm{sSet}⟨{B},{D}⟩\right)\mathrm{sSet}⟨{A},{C}⟩$