# Metamath Proof Explorer

## Theorem propeqop

Description: Equivalence for an ordered pair equal to a pair of ordered pairs. (Contributed by AV, 18-Sep-2020) (Proof shortened by AV, 16-Jun-2022) (Avoid depending on this detail.)

Ref Expression
Hypotheses snopeqop.a ${⊢}{A}\in \mathrm{V}$
snopeqop.b ${⊢}{B}\in \mathrm{V}$
propeqop.c ${⊢}{C}\in \mathrm{V}$
propeqop.d ${⊢}{D}\in \mathrm{V}$
propeqop.e ${⊢}{E}\in \mathrm{V}$
propeqop.f ${⊢}{F}\in \mathrm{V}$
Assertion propeqop ${⊢}\left\{⟨{A},{B}⟩,⟨{C},{D}⟩\right\}=⟨{E},{F}⟩↔\left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\vee \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 snopeqop.a ${⊢}{A}\in \mathrm{V}$
2 snopeqop.b ${⊢}{B}\in \mathrm{V}$
3 propeqop.c ${⊢}{C}\in \mathrm{V}$
4 propeqop.d ${⊢}{D}\in \mathrm{V}$
5 propeqop.e ${⊢}{E}\in \mathrm{V}$
6 propeqop.f ${⊢}{F}\in \mathrm{V}$
7 1 2 opeqsn ${⊢}⟨{A},{B}⟩=\left\{{E}\right\}↔\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)$
8 3 4 5 6 opeqpr ${⊢}⟨{C},{D}⟩=\left\{{E},{F}\right\}↔\left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)$
9 7 8 anbi12i ${⊢}\left(⟨{A},{B}⟩=\left\{{E}\right\}\wedge ⟨{C},{D}⟩=\left\{{E},{F}\right\}\right)↔\left(\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\right)$
10 1 2 5 6 opeqpr ${⊢}⟨{A},{B}⟩=\left\{{E},{F}\right\}↔\left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\vee \left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\right)$
11 3 4 opeqsn ${⊢}⟨{C},{D}⟩=\left\{{E}\right\}↔\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)$
12 10 11 anbi12i ${⊢}\left(⟨{A},{B}⟩=\left\{{E},{F}\right\}\wedge ⟨{C},{D}⟩=\left\{{E}\right\}\right)↔\left(\left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\vee \left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\right)\wedge \left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\right)$
13 9 12 orbi12i ${⊢}\left(\left(⟨{A},{B}⟩=\left\{{E}\right\}\wedge ⟨{C},{D}⟩=\left\{{E},{F}\right\}\right)\vee \left(⟨{A},{B}⟩=\left\{{E},{F}\right\}\wedge ⟨{C},{D}⟩=\left\{{E}\right\}\right)\right)↔\left(\left(\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\right)\vee \left(\left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\vee \left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\right)\wedge \left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\right)\right)$
14 eqcom ${⊢}\left\{⟨{A},{B}⟩,⟨{C},{D}⟩\right\}=⟨{E},{F}⟩↔⟨{E},{F}⟩=\left\{⟨{A},{B}⟩,⟨{C},{D}⟩\right\}$
15 opex ${⊢}⟨{A},{B}⟩\in \mathrm{V}$
16 opex ${⊢}⟨{C},{D}⟩\in \mathrm{V}$
17 5 6 15 16 opeqpr ${⊢}⟨{E},{F}⟩=\left\{⟨{A},{B}⟩,⟨{C},{D}⟩\right\}↔\left(\left(⟨{A},{B}⟩=\left\{{E}\right\}\wedge ⟨{C},{D}⟩=\left\{{E},{F}\right\}\right)\vee \left(⟨{A},{B}⟩=\left\{{E},{F}\right\}\wedge ⟨{C},{D}⟩=\left\{{E}\right\}\right)\right)$
18 14 17 bitri ${⊢}\left\{⟨{A},{B}⟩,⟨{C},{D}⟩\right\}=⟨{E},{F}⟩↔\left(\left(⟨{A},{B}⟩=\left\{{E}\right\}\wedge ⟨{C},{D}⟩=\left\{{E},{F}\right\}\right)\vee \left(⟨{A},{B}⟩=\left\{{E},{F}\right\}\wedge ⟨{C},{D}⟩=\left\{{E}\right\}\right)\right)$
19 simpl ${⊢}\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\to {A}={B}$
20 simpr ${⊢}\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\to {E}=\left\{{A}\right\}$
21 19 20 anim12i ${⊢}\left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\wedge \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\to \left({A}={B}\wedge {E}=\left\{{A}\right\}\right)$
22 sneq ${⊢}{A}={C}\to \left\{{A}\right\}=\left\{{C}\right\}$
23 22 eqeq2d ${⊢}{A}={C}\to \left({E}=\left\{{A}\right\}↔{E}=\left\{{C}\right\}\right)$
24 23 biimpa ${⊢}\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\to {E}=\left\{{C}\right\}$
25 24 adantl ${⊢}\left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\wedge \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\to {E}=\left\{{C}\right\}$
26 preq1 ${⊢}{A}={C}\to \left\{{A},{D}\right\}=\left\{{C},{D}\right\}$
27 26 adantr ${⊢}\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\to \left\{{A},{D}\right\}=\left\{{C},{D}\right\}$
28 27 eqeq2d ${⊢}\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\to \left({F}=\left\{{A},{D}\right\}↔{F}=\left\{{C},{D}\right\}\right)$
29 28 biimpcd ${⊢}{F}=\left\{{A},{D}\right\}\to \left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\to {F}=\left\{{C},{D}\right\}\right)$
30 29 adantl ${⊢}\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\to \left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\to {F}=\left\{{C},{D}\right\}\right)$
31 30 imp ${⊢}\left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\wedge \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\to {F}=\left\{{C},{D}\right\}$
32 25 31 jca ${⊢}\left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\wedge \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\to \left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)$
33 32 orcd ${⊢}\left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\wedge \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\to \left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)$
34 21 33 jca ${⊢}\left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\wedge \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\to \left(\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\right)$
35 34 orcd ${⊢}\left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\wedge \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\to \left(\left(\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\right)\vee \left(\left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\vee \left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\right)\wedge \left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\right)\right)$
36 35 ex ${⊢}\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\to \left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\to \left(\left(\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\right)\vee \left(\left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\vee \left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\right)\wedge \left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\right)\right)\right)$
37 simpr ${⊢}\left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\to {F}=\left\{{A},{B}\right\}$
38 20 37 anim12i ${⊢}\left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\wedge \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\to \left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)$
39 38 ancoms ${⊢}\left(\left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\wedge \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\to \left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)$
40 39 orcd ${⊢}\left(\left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\wedge \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\to \left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\vee \left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\right)$
41 simpl ${⊢}\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\to {A}={C}$
42 41 eqeq1d ${⊢}\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\to \left({A}={D}↔{C}={D}\right)$
43 42 biimpcd ${⊢}{A}={D}\to \left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\to {C}={D}\right)$
44 43 adantr ${⊢}\left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\to \left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\to {C}={D}\right)$
45 44 imp ${⊢}\left(\left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\wedge \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\to {C}={D}$
46 23 biimpd ${⊢}{A}={C}\to \left({E}=\left\{{A}\right\}\to {E}=\left\{{C}\right\}\right)$
47 46 a1dd ${⊢}{A}={C}\to \left({E}=\left\{{A}\right\}\to \left(\left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\to {E}=\left\{{C}\right\}\right)\right)$
48 47 imp ${⊢}\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\to \left(\left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\to {E}=\left\{{C}\right\}\right)$
49 48 impcom ${⊢}\left(\left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\wedge \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\to {E}=\left\{{C}\right\}$
50 45 49 jca ${⊢}\left(\left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\wedge \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\to \left({C}={D}\wedge {E}=\left\{{C}\right\}\right)$
51 40 50 jca ${⊢}\left(\left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\wedge \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\to \left(\left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\vee \left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\right)\wedge \left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\right)$
52 51 olcd ${⊢}\left(\left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\wedge \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\to \left(\left(\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\right)\vee \left(\left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\vee \left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\right)\wedge \left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\right)\right)$
53 52 ex ${⊢}\left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\to \left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\to \left(\left(\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\right)\vee \left(\left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\vee \left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\right)\wedge \left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\right)\right)\right)$
54 36 53 jaoi ${⊢}\left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\vee \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\to \left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\to \left(\left(\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\right)\vee \left(\left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\vee \left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\right)\wedge \left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\right)\right)\right)$
55 54 impcom ${⊢}\left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\vee \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)\to \left(\left(\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\right)\vee \left(\left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\vee \left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\right)\wedge \left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\right)\right)$
56 eqeq1 ${⊢}{E}=\left\{{C}\right\}\to \left({E}=\left\{{A}\right\}↔\left\{{C}\right\}=\left\{{A}\right\}\right)$
57 3 sneqr ${⊢}\left\{{C}\right\}=\left\{{A}\right\}\to {C}={A}$
58 57 eqcomd ${⊢}\left\{{C}\right\}=\left\{{A}\right\}\to {A}={C}$
59 56 58 syl6bi ${⊢}{E}=\left\{{C}\right\}\to \left({E}=\left\{{A}\right\}\to {A}={C}\right)$
60 59 adantr ${⊢}\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\to \left({E}=\left\{{A}\right\}\to {A}={C}\right)$
61 eqeq1 ${⊢}{E}=\left\{{C},{D}\right\}\to \left({E}=\left\{{A}\right\}↔\left\{{C},{D}\right\}=\left\{{A}\right\}\right)$
62 3 4 preqsn ${⊢}\left\{{C},{D}\right\}=\left\{{A}\right\}↔\left({C}={D}\wedge {D}={A}\right)$
63 eqtr ${⊢}\left({C}={D}\wedge {D}={A}\right)\to {C}={A}$
64 63 eqcomd ${⊢}\left({C}={D}\wedge {D}={A}\right)\to {A}={C}$
65 62 64 sylbi ${⊢}\left\{{C},{D}\right\}=\left\{{A}\right\}\to {A}={C}$
66 61 65 syl6bi ${⊢}{E}=\left\{{C},{D}\right\}\to \left({E}=\left\{{A}\right\}\to {A}={C}\right)$
67 66 adantr ${⊢}\left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\to \left({E}=\left\{{A}\right\}\to {A}={C}\right)$
68 60 67 jaoi ${⊢}\left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\to \left({E}=\left\{{A}\right\}\to {A}={C}\right)$
69 68 com12 ${⊢}{E}=\left\{{A}\right\}\to \left(\left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\to {A}={C}\right)$
70 69 adantl ${⊢}\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\to \left(\left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\to {A}={C}\right)$
71 70 impcom ${⊢}\left(\left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\wedge \left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\right)\to {A}={C}$
72 simpr ${⊢}\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\to {E}=\left\{{A}\right\}$
73 72 adantl ${⊢}\left(\left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\wedge \left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\right)\to {E}=\left\{{A}\right\}$
74 71 73 jca ${⊢}\left(\left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\wedge \left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\right)\to \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)$
75 simpl ${⊢}\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\to {A}={B}$
76 75 adantr ${⊢}\left(\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\wedge \left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\right)\to {A}={B}$
77 eqeq1 ${⊢}{E}=\left\{{A}\right\}\to \left({E}=\left\{{C}\right\}↔\left\{{A}\right\}=\left\{{C}\right\}\right)$
78 1 sneqr ${⊢}\left\{{A}\right\}=\left\{{C}\right\}\to {A}={C}$
79 78 eqcomd ${⊢}\left\{{A}\right\}=\left\{{C}\right\}\to {C}={A}$
80 77 79 syl6bi ${⊢}{E}=\left\{{A}\right\}\to \left({E}=\left\{{C}\right\}\to {C}={A}\right)$
81 80 adantl ${⊢}\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\to \left({E}=\left\{{C}\right\}\to {C}={A}\right)$
82 81 impcom ${⊢}\left({E}=\left\{{C}\right\}\wedge \left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\right)\to {C}={A}$
83 82 preq1d ${⊢}\left({E}=\left\{{C}\right\}\wedge \left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\right)\to \left\{{C},{D}\right\}=\left\{{A},{D}\right\}$
84 83 eqeq2d ${⊢}\left({E}=\left\{{C}\right\}\wedge \left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\right)\to \left({F}=\left\{{C},{D}\right\}↔{F}=\left\{{A},{D}\right\}\right)$
85 84 biimpd ${⊢}\left({E}=\left\{{C}\right\}\wedge \left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\right)\to \left({F}=\left\{{C},{D}\right\}\to {F}=\left\{{A},{D}\right\}\right)$
86 85 impancom ${⊢}\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\to \left(\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\to {F}=\left\{{A},{D}\right\}\right)$
87 86 impcom ${⊢}\left(\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\wedge \left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\right)\to {F}=\left\{{A},{D}\right\}$
88 76 87 jca ${⊢}\left(\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\wedge \left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\right)\to \left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)$
89 88 ex ${⊢}\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\to \left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\to \left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\right)$
90 eqcom ${⊢}{D}={A}↔{A}={D}$
91 90 biimpi ${⊢}{D}={A}\to {A}={D}$
92 91 adantl ${⊢}\left({C}={D}\wedge {D}={A}\right)\to {A}={D}$
93 92 adantr ${⊢}\left(\left({C}={D}\wedge {D}={A}\right)\wedge {A}={B}\right)\to {A}={D}$
94 93 adantr ${⊢}\left(\left(\left({C}={D}\wedge {D}={A}\right)\wedge {A}={B}\right)\wedge {F}=\left\{{C}\right\}\right)\to {A}={D}$
95 simpr ${⊢}\left(\left({C}={D}\wedge {D}={A}\right)\wedge {A}={B}\right)\to {A}={B}$
96 64 eqeq1d ${⊢}\left({C}={D}\wedge {D}={A}\right)\to \left({A}={B}↔{C}={B}\right)$
97 96 biimpa ${⊢}\left(\left({C}={D}\wedge {D}={A}\right)\wedge {A}={B}\right)\to {C}={B}$
98 97 eqcomd ${⊢}\left(\left({C}={D}\wedge {D}={A}\right)\wedge {A}={B}\right)\to {B}={C}$
99 1 2 preqsn ${⊢}\left\{{A},{B}\right\}=\left\{{C}\right\}↔\left({A}={B}\wedge {B}={C}\right)$
100 95 98 99 sylanbrc ${⊢}\left(\left({C}={D}\wedge {D}={A}\right)\wedge {A}={B}\right)\to \left\{{A},{B}\right\}=\left\{{C}\right\}$
101 100 eqcomd ${⊢}\left(\left({C}={D}\wedge {D}={A}\right)\wedge {A}={B}\right)\to \left\{{C}\right\}=\left\{{A},{B}\right\}$
102 101 eqeq2d ${⊢}\left(\left({C}={D}\wedge {D}={A}\right)\wedge {A}={B}\right)\to \left({F}=\left\{{C}\right\}↔{F}=\left\{{A},{B}\right\}\right)$
103 102 biimpa ${⊢}\left(\left(\left({C}={D}\wedge {D}={A}\right)\wedge {A}={B}\right)\wedge {F}=\left\{{C}\right\}\right)\to {F}=\left\{{A},{B}\right\}$
104 94 103 jca ${⊢}\left(\left(\left({C}={D}\wedge {D}={A}\right)\wedge {A}={B}\right)\wedge {F}=\left\{{C}\right\}\right)\to \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)$
105 104 ex ${⊢}\left(\left({C}={D}\wedge {D}={A}\right)\wedge {A}={B}\right)\to \left({F}=\left\{{C}\right\}\to \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)$
106 105 ex ${⊢}\left({C}={D}\wedge {D}={A}\right)\to \left({A}={B}\to \left({F}=\left\{{C}\right\}\to \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)$
107 106 com23 ${⊢}\left({C}={D}\wedge {D}={A}\right)\to \left({F}=\left\{{C}\right\}\to \left({A}={B}\to \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)$
108 62 107 sylbi ${⊢}\left\{{C},{D}\right\}=\left\{{A}\right\}\to \left({F}=\left\{{C}\right\}\to \left({A}={B}\to \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)$
109 61 108 syl6bi ${⊢}{E}=\left\{{C},{D}\right\}\to \left({E}=\left\{{A}\right\}\to \left({F}=\left\{{C}\right\}\to \left({A}={B}\to \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)\right)$
110 109 com23 ${⊢}{E}=\left\{{C},{D}\right\}\to \left({F}=\left\{{C}\right\}\to \left({E}=\left\{{A}\right\}\to \left({A}={B}\to \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)\right)$
111 110 imp ${⊢}\left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\to \left({E}=\left\{{A}\right\}\to \left({A}={B}\to \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)$
112 111 com13 ${⊢}{A}={B}\to \left({E}=\left\{{A}\right\}\to \left(\left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\to \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)$
113 112 imp ${⊢}\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\to \left(\left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\to \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)$
114 89 113 orim12d ${⊢}\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\to \left(\left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\to \left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\vee \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)$
115 114 impcom ${⊢}\left(\left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\wedge \left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\right)\to \left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\vee \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)$
116 74 115 jca ${⊢}\left(\left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\wedge \left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\right)\to \left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\vee \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)$
117 116 ancoms ${⊢}\left(\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\right)\to \left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\vee \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)$
118 eqeq1 ${⊢}{E}=\left\{{C}\right\}\to \left({E}=\left\{{A},{B}\right\}↔\left\{{C}\right\}=\left\{{A},{B}\right\}\right)$
119 eqcom ${⊢}\left\{{C}\right\}=\left\{{A},{B}\right\}↔\left\{{A},{B}\right\}=\left\{{C}\right\}$
120 119 99 bitri ${⊢}\left\{{C}\right\}=\left\{{A},{B}\right\}↔\left({A}={B}\wedge {B}={C}\right)$
121 eqtr ${⊢}\left({A}={B}\wedge {B}={C}\right)\to {A}={C}$
122 121 adantr ${⊢}\left(\left({A}={B}\wedge {B}={C}\right)\wedge {E}=\left\{{C}\right\}\right)\to {A}={C}$
123 121 eqcomd ${⊢}\left({A}={B}\wedge {B}={C}\right)\to {C}={A}$
124 sneq ${⊢}{C}={A}\to \left\{{C}\right\}=\left\{{A}\right\}$
125 123 124 syl ${⊢}\left({A}={B}\wedge {B}={C}\right)\to \left\{{C}\right\}=\left\{{A}\right\}$
126 125 eqeq2d ${⊢}\left({A}={B}\wedge {B}={C}\right)\to \left({E}=\left\{{C}\right\}↔{E}=\left\{{A}\right\}\right)$
127 126 biimpa ${⊢}\left(\left({A}={B}\wedge {B}={C}\right)\wedge {E}=\left\{{C}\right\}\right)\to {E}=\left\{{A}\right\}$
128 122 127 jca ${⊢}\left(\left({A}={B}\wedge {B}={C}\right)\wedge {E}=\left\{{C}\right\}\right)\to \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)$
129 128 ex ${⊢}\left({A}={B}\wedge {B}={C}\right)\to \left({E}=\left\{{C}\right\}\to \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)$
130 129 a1i13 ${⊢}{C}={D}\to \left(\left({A}={B}\wedge {B}={C}\right)\to \left({F}=\left\{{A}\right\}\to \left({E}=\left\{{C}\right\}\to \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\right)\right)$
131 130 com14 ${⊢}{E}=\left\{{C}\right\}\to \left(\left({A}={B}\wedge {B}={C}\right)\to \left({F}=\left\{{A}\right\}\to \left({C}={D}\to \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\right)\right)$
132 120 131 syl5bi ${⊢}{E}=\left\{{C}\right\}\to \left(\left\{{C}\right\}=\left\{{A},{B}\right\}\to \left({F}=\left\{{A}\right\}\to \left({C}={D}\to \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\right)\right)$
133 118 132 sylbid ${⊢}{E}=\left\{{C}\right\}\to \left({E}=\left\{{A},{B}\right\}\to \left({F}=\left\{{A}\right\}\to \left({C}={D}\to \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\right)\right)$
134 133 com24 ${⊢}{E}=\left\{{C}\right\}\to \left({C}={D}\to \left({F}=\left\{{A}\right\}\to \left({E}=\left\{{A},{B}\right\}\to \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\right)\right)$
135 134 impcom ${⊢}\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\to \left({F}=\left\{{A}\right\}\to \left({E}=\left\{{A},{B}\right\}\to \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\right)$
136 135 com13 ${⊢}{E}=\left\{{A},{B}\right\}\to \left({F}=\left\{{A}\right\}\to \left(\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\to \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)\right)$
137 136 imp ${⊢}\left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\to \left(\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\to \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)$
138 59 adantl ${⊢}\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\to \left({E}=\left\{{A}\right\}\to {A}={C}\right)$
139 138 com12 ${⊢}{E}=\left\{{A}\right\}\to \left(\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\to {A}={C}\right)$
140 139 adantr ${⊢}\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\to \left(\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\to {A}={C}\right)$
141 140 imp ${⊢}\left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\wedge \left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\right)\to {A}={C}$
142 simpl ${⊢}\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\to {E}=\left\{{A}\right\}$
143 142 adantr ${⊢}\left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\wedge \left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\right)\to {E}=\left\{{A}\right\}$
144 141 143 jca ${⊢}\left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\wedge \left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\right)\to \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)$
145 144 ex ${⊢}\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\to \left(\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\to \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)$
146 137 145 jaoi ${⊢}\left(\left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\vee \left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\to \left(\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\to \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\right)$
147 146 impcom ${⊢}\left(\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\wedge \left(\left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\vee \left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)\to \left({A}={C}\wedge {E}=\left\{{A}\right\}\right)$
148 eqeq1 ${⊢}{E}=\left\{{A},{B}\right\}\to \left({E}=\left\{{C}\right\}↔\left\{{A},{B}\right\}=\left\{{C}\right\}\right)$
149 simpl ${⊢}\left({A}={B}\wedge {B}={C}\right)\to {A}={B}$
150 149 adantr ${⊢}\left(\left({A}={B}\wedge {B}={C}\right)\wedge {C}={D}\right)\to {A}={B}$
151 150 adantr ${⊢}\left(\left(\left({A}={B}\wedge {B}={C}\right)\wedge {C}={D}\right)\wedge {F}=\left\{{A}\right\}\right)\to {A}={B}$
152 eqtr ${⊢}\left({A}={C}\wedge {C}={D}\right)\to {A}={D}$
153 dfsn2 ${⊢}\left\{{A}\right\}=\left\{{A},{A}\right\}$
154 preq2 ${⊢}{A}={D}\to \left\{{A},{A}\right\}=\left\{{A},{D}\right\}$
155 153 154 syl5eq ${⊢}{A}={D}\to \left\{{A}\right\}=\left\{{A},{D}\right\}$
156 152 155 syl ${⊢}\left({A}={C}\wedge {C}={D}\right)\to \left\{{A}\right\}=\left\{{A},{D}\right\}$
157 156 ex ${⊢}{A}={C}\to \left({C}={D}\to \left\{{A}\right\}=\left\{{A},{D}\right\}\right)$
158 121 157 syl ${⊢}\left({A}={B}\wedge {B}={C}\right)\to \left({C}={D}\to \left\{{A}\right\}=\left\{{A},{D}\right\}\right)$
159 158 imp ${⊢}\left(\left({A}={B}\wedge {B}={C}\right)\wedge {C}={D}\right)\to \left\{{A}\right\}=\left\{{A},{D}\right\}$
160 159 eqeq2d ${⊢}\left(\left({A}={B}\wedge {B}={C}\right)\wedge {C}={D}\right)\to \left({F}=\left\{{A}\right\}↔{F}=\left\{{A},{D}\right\}\right)$
161 160 biimpa ${⊢}\left(\left(\left({A}={B}\wedge {B}={C}\right)\wedge {C}={D}\right)\wedge {F}=\left\{{A}\right\}\right)\to {F}=\left\{{A},{D}\right\}$
162 151 161 jca ${⊢}\left(\left(\left({A}={B}\wedge {B}={C}\right)\wedge {C}={D}\right)\wedge {F}=\left\{{A}\right\}\right)\to \left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)$
163 162 ex ${⊢}\left(\left({A}={B}\wedge {B}={C}\right)\wedge {C}={D}\right)\to \left({F}=\left\{{A}\right\}\to \left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\right)$
164 163 ex ${⊢}\left({A}={B}\wedge {B}={C}\right)\to \left({C}={D}\to \left({F}=\left\{{A}\right\}\to \left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\right)\right)$
165 164 com23 ${⊢}\left({A}={B}\wedge {B}={C}\right)\to \left({F}=\left\{{A}\right\}\to \left({C}={D}\to \left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\right)\right)$
166 99 165 sylbi ${⊢}\left\{{A},{B}\right\}=\left\{{C}\right\}\to \left({F}=\left\{{A}\right\}\to \left({C}={D}\to \left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\right)\right)$
167 148 166 syl6bi ${⊢}{E}=\left\{{A},{B}\right\}\to \left({E}=\left\{{C}\right\}\to \left({F}=\left\{{A}\right\}\to \left({C}={D}\to \left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\right)\right)\right)$
168 167 com23 ${⊢}{E}=\left\{{A},{B}\right\}\to \left({F}=\left\{{A}\right\}\to \left({E}=\left\{{C}\right\}\to \left({C}={D}\to \left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\right)\right)\right)$
169 168 imp ${⊢}\left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\to \left({E}=\left\{{C}\right\}\to \left({C}={D}\to \left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\right)\right)$
170 169 com13 ${⊢}{C}={D}\to \left({E}=\left\{{C}\right\}\to \left(\left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\to \left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\right)\right)$
171 170 imp ${⊢}\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\to \left(\left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\to \left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\right)$
172 80 imp ${⊢}\left({E}=\left\{{A}\right\}\wedge {E}=\left\{{C}\right\}\right)\to {C}={A}$
173 172 eqeq1d ${⊢}\left({E}=\left\{{A}\right\}\wedge {E}=\left\{{C}\right\}\right)\to \left({C}={D}↔{A}={D}\right)$
174 173 biimpd ${⊢}\left({E}=\left\{{A}\right\}\wedge {E}=\left\{{C}\right\}\right)\to \left({C}={D}\to {A}={D}\right)$
175 174 ex ${⊢}{E}=\left\{{A}\right\}\to \left({E}=\left\{{C}\right\}\to \left({C}={D}\to {A}={D}\right)\right)$
176 175 com13 ${⊢}{C}={D}\to \left({E}=\left\{{C}\right\}\to \left({E}=\left\{{A}\right\}\to {A}={D}\right)\right)$
177 176 imp ${⊢}\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\to \left({E}=\left\{{A}\right\}\to {A}={D}\right)$
178 177 anim1d ${⊢}\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\to \left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\to \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)$
179 171 178 orim12d ${⊢}\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\to \left(\left(\left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\vee \left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\to \left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\vee \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)$
180 179 imp ${⊢}\left(\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\wedge \left(\left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\vee \left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)\to \left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\vee \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)$
181 147 180 jca ${⊢}\left(\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\wedge \left(\left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\vee \left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)\to \left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\vee \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)$
182 181 ex ${⊢}\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\to \left(\left(\left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\vee \left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\to \left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\vee \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)\right)$
183 182 com12 ${⊢}\left(\left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\vee \left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\to \left(\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\to \left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\vee \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)\right)$
184 183 orcoms ${⊢}\left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\vee \left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\right)\to \left(\left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\to \left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\vee \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)\right)$
185 184 imp ${⊢}\left(\left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\vee \left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\right)\wedge \left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\right)\to \left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\vee \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)$
186 117 185 jaoi ${⊢}\left(\left(\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\right)\vee \left(\left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\vee \left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\right)\wedge \left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\right)\right)\to \left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\vee \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)$
187 55 186 impbii ${⊢}\left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\vee \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)↔\left(\left(\left({A}={B}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({E}=\left\{{C}\right\}\wedge {F}=\left\{{C},{D}\right\}\right)\vee \left({E}=\left\{{C},{D}\right\}\wedge {F}=\left\{{C}\right\}\right)\right)\right)\vee \left(\left(\left({E}=\left\{{A}\right\}\wedge {F}=\left\{{A},{B}\right\}\right)\vee \left({E}=\left\{{A},{B}\right\}\wedge {F}=\left\{{A}\right\}\right)\right)\wedge \left({C}={D}\wedge {E}=\left\{{C}\right\}\right)\right)\right)$
188 13 18 187 3bitr4i ${⊢}\left\{⟨{A},{B}⟩,⟨{C},{D}⟩\right\}=⟨{E},{F}⟩↔\left(\left({A}={C}\wedge {E}=\left\{{A}\right\}\right)\wedge \left(\left({A}={B}\wedge {F}=\left\{{A},{D}\right\}\right)\vee \left({A}={D}\wedge {F}=\left\{{A},{B}\right\}\right)\right)\right)$