This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ V
snopeqop.b ⊢ 𝐵 ∈ V
propeqop.c ⊢ 𝐶 ∈ V
propeqop.d ⊢ 𝐷 ∈ V
propeqop.e ⊢ 𝐸 ∈ V
propeqop.f ⊢ 𝐹 ∈ V
Assertion propeqop ( { ⟨ 𝐴 , 𝐵 ⟩ , ⟨ 𝐶 , 𝐷 ⟩ } = ⟨ 𝐸 , 𝐹 ⟩ ↔ ( ( 𝐴 = 𝐶 ∧ 𝐸 = { 𝐴 } ) ∧ ( ( 𝐴 = 𝐵 ∧ 𝐹 = { 𝐴 , 𝐷 } ) ∨ ( 𝐴 = 𝐷 ∧ 𝐹 = { 𝐴 , 𝐵 } ) ) ) )

Proof

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