Theorem propeqop 5389

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.)

Hypotheses

Ref	Expression
snopeqop.a	⊢ 𝐴 ∈ V
snopeqop.b	⊢ 𝐵 ∈ V
propeqop.c	⊢ 𝐶 ∈ V
propeqop.d	⊢ 𝐷 ∈ V
propeqop.e	⊢ 𝐸 ∈ V
propeqop.f	⊢ 𝐹 ∈ V

Assertion

Ref	Expression
propeqop	⊢ ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ⟨𝐸, 𝐹⟩ ↔ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))

Proof of Theorem propeqop

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   = wceq 1533   ∈ wcel 2110  Vcvv 3494  {csn 4560  {cpr 4562  ⟨cop 4566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567

This theorem is referenced by:  propssopi  5390  fun2dmnopgexmpl  43477