Theorem propeqop 4895

Description: Equivalence for an ordered pair equal to a pair of ordered pairs. (Contributed by AV, 18-Sep-2020.)

Hypotheses

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

Syntax hints:   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977  Vcvv 3173  {csn 4125  {cpr 4127  ⟨cop 4131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132

This theorem is referenced by:  propssopi  4896  fun2dmnopgexmpl  40329