Theorem propeqop 5455

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 5452	. . . 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 5453	. . . 4 ⊢ (⟨𝐶, 𝐷⟩ = {𝐸, 𝐹} ↔ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})))
9	3, 8	anbi12i 634	. . 3 ⊢ ((⟨𝐴, 𝐵⟩ = {𝐸} ∧ ⟨𝐶, 𝐷⟩ = {𝐸, 𝐹}) ↔ ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))))
10	1, 2, 6, 7	opeqpr 5453	. . . 4 ⊢ (⟨𝐴, 𝐵⟩ = {𝐸, 𝐹} ↔ ((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})))
11	4, 5	opeqsn 5452	. . . 4 ⊢ (⟨𝐶, 𝐷⟩ = {𝐸} ↔ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶}))
12	10, 11	anbi12i 634	. . 3 ⊢ ((⟨𝐴, 𝐵⟩ = {𝐸, 𝐹} ∧ ⟨𝐶, 𝐷⟩ = {𝐸}) ↔ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})))
13	9, 12	orbi12i 920	. 2 ⊢ (((⟨𝐴, 𝐵⟩ = {𝐸} ∧ ⟨𝐶, 𝐷⟩ = {𝐸, 𝐹}) ∨ (⟨𝐴, 𝐵⟩ = {𝐸, 𝐹} ∧ ⟨𝐶, 𝐷⟩ = {𝐸})) ↔ (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) ∨ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶}))))
14		eqcom 2747	. . 3 ⊢ ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ⟨𝐸, 𝐹⟩ ↔ ⟨𝐸, 𝐹⟩ = {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩})
15		opex 5410	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ ∈ V
16		opex 5410	. . . 4 ⊢ ⟨𝐶, 𝐷⟩ ∈ V
17	6, 7, 15, 16	opeqpr 5453	. . 3 ⊢ (⟨𝐸, 𝐹⟩ = {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ↔ ((⟨𝐴, 𝐵⟩ = {𝐸} ∧ ⟨𝐶, 𝐷⟩ = {𝐸, 𝐹}) ∨ (⟨𝐴, 𝐵⟩ = {𝐸, 𝐹} ∧ ⟨𝐶, 𝐷⟩ = {𝐸})))
18	14, 17	bitri 276	. 2 ⊢ ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ⟨𝐸, 𝐹⟩ ↔ ((⟨𝐴, 𝐵⟩ = {𝐸} ∧ ⟨𝐶, 𝐷⟩ = {𝐸, 𝐹}) ∨ (⟨𝐴, 𝐵⟩ = {𝐸, 𝐹} ∧ ⟨𝐶, 𝐷⟩ = {𝐸})))
19		simpl 483	. . . . . . . . 9 ⊢ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) → 𝐴 = 𝐵)
20		simpr 485	. . . . . . . . 9 ⊢ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → 𝐸 = {𝐴})
21	19, 20	anim12i 619	. . . . . . . 8 ⊢ (((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → (𝐴 = 𝐵 ∧ 𝐸 = {𝐴}))
22		sneq 4572	. . . . . . . . . . . . 13 ⊢ (𝐴 = 𝐶 → {𝐴} = {𝐶})
23	22	eqeq2d 2751	. . . . . . . . . . . 12 ⊢ (𝐴 = 𝐶 → (𝐸 = {𝐴} ↔ 𝐸 = {𝐶}))
24	23	biimpa 477	. . . . . . . . . . 11 ⊢ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → 𝐸 = {𝐶})
25	24	adantl 482	. . . . . . . . . 10 ⊢ (((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → 𝐸 = {𝐶})
26		preq1 4672	. . . . . . . . . . . . . . 15 ⊢ (𝐴 = 𝐶 → {𝐴, 𝐷} = {𝐶, 𝐷})
27	26	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → {𝐴, 𝐷} = {𝐶, 𝐷})
28	27	eqeq2d 2751	. . . . . . . . . . . . 13 ⊢ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → (𝐹 = {𝐴, 𝐷} ↔ 𝐹 = {𝐶, 𝐷}))
29	28	biimpcd 250	. . . . . . . . . . . 12 ⊢ (𝐹 = {𝐴, 𝐷} → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → 𝐹 = {𝐶, 𝐷}))
30	29	adantl 482	. . . . . . . . . . 11 ⊢ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → 𝐹 = {𝐶, 𝐷}))
31	30	imp 407	. . . . . . . . . 10 ⊢ (((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → 𝐹 = {𝐶, 𝐷})
32	25, 31	jca 516	. . . . . . . . 9 ⊢ (((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → (𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}))
33	32	orcd 879	. . . . . . . 8 ⊢ (((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})))
34	21, 33	jca 516	. . . . . . 7 ⊢ (((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))))
35	34	orcd 879	. . . . . 6 ⊢ (((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) ∨ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶}))))
36	35	ex 413	. . . . 5 ⊢ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) ∨ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})))))
37		simpr 485	. . . . . . . . . . 11 ⊢ ((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) → 𝐹 = {𝐴, 𝐵})
38	20, 37	anim12i 619	. . . . . . . . . 10 ⊢ (((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})) → (𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}))
39	38	ancoms 459	. . . . . . . . 9 ⊢ (((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → (𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}))
40	39	orcd 879	. . . . . . . 8 ⊢ (((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → ((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})))
41		simpl 483	. . . . . . . . . . . . 13 ⊢ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → 𝐴 = 𝐶)
42	41	eqeq1d 2742	. . . . . . . . . . . 12 ⊢ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → (𝐴 = 𝐷 ↔ 𝐶 = 𝐷))
43	42	biimpcd 250	. . . . . . . . . . 11 ⊢ (𝐴 = 𝐷 → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → 𝐶 = 𝐷))
44	43	adantr 481	. . . . . . . . . 10 ⊢ ((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → 𝐶 = 𝐷))
45	44	imp 407	. . . . . . . . 9 ⊢ (((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → 𝐶 = 𝐷)
46	23	biimpd 230	. . . . . . . . . . . 12 ⊢ (𝐴 = 𝐶 → (𝐸 = {𝐴} → 𝐸 = {𝐶}))
47	46	a1dd 50	. . . . . . . . . . 11 ⊢ (𝐴 = 𝐶 → (𝐸 = {𝐴} → ((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) → 𝐸 = {𝐶})))
48	47	imp 407	. . . . . . . . . 10 ⊢ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → ((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) → 𝐸 = {𝐶}))
49	48	impcom 408	. . . . . . . . 9 ⊢ (((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → 𝐸 = {𝐶})
50	45, 49	jca 516	. . . . . . . 8 ⊢ (((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → (𝐶 = 𝐷 ∧ 𝐸 = {𝐶}))
51	40, 50	jca 516	. . . . . . 7 ⊢ (((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})))
52	51	olcd 880	. . . . . 6 ⊢ (((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) ∨ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶}))))
53	52	ex 413	. . . . 5 ⊢ ((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) ∨ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})))))
54	36, 53	jaoi 863	. . . 4 ⊢ (((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) ∨ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})))))
55	54	impcom 408	. . 3 ⊢ (((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))) → (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) ∨ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶}))))
56		eqeq1 2744	. . . . . . . . . . . . 13 ⊢ (𝐸 = {𝐶} → (𝐸 = {𝐴} ↔ {𝐶} = {𝐴}))
57	4	sneqr 4778	. . . . . . . . . . . . . 14 ⊢ ({𝐶} = {𝐴} → 𝐶 = 𝐴)
58	57	eqcomd 2746	. . . . . . . . . . . . 13 ⊢ ({𝐶} = {𝐴} → 𝐴 = 𝐶)
59	56, 58	biimtrdi 254	. . . . . . . . . . . 12 ⊢ (𝐸 = {𝐶} → (𝐸 = {𝐴} → 𝐴 = 𝐶))
60	59	adantr 481	. . . . . . . . . . 11 ⊢ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) → (𝐸 = {𝐴} → 𝐴 = 𝐶))
61		eqeq1 2744	. . . . . . . . . . . . 13 ⊢ (𝐸 = {𝐶, 𝐷} → (𝐸 = {𝐴} ↔ {𝐶, 𝐷} = {𝐴}))
62	4, 5	preqsn 4800	. . . . . . . . . . . . . 14 ⊢ ({𝐶, 𝐷} = {𝐴} ↔ (𝐶 = 𝐷 ∧ 𝐷 = 𝐴))
63		eqtr 2760	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) → 𝐶 = 𝐴)
64	63	eqcomd 2746	. . . . . . . . . . . . . 14 ⊢ ((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) → 𝐴 = 𝐶)
65	62, 64	sylbi 218	. . . . . . . . . . . . 13 ⊢ ({𝐶, 𝐷} = {𝐴} → 𝐴 = 𝐶)
66	61, 65	biimtrdi 254	. . . . . . . . . . . 12 ⊢ (𝐸 = {𝐶, 𝐷} → (𝐸 = {𝐴} → 𝐴 = 𝐶))
67	66	adantr 481	. . . . . . . . . . 11 ⊢ ((𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}) → (𝐸 = {𝐴} → 𝐴 = 𝐶))
68	60, 67	jaoi 863	. . . . . . . . . 10 ⊢ (((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})) → (𝐸 = {𝐴} → 𝐴 = 𝐶))
69	68	com12 32	. . . . . . . . 9 ⊢ (𝐸 = {𝐴} → (((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})) → 𝐴 = 𝐶))
70	69	adantl 482	. . . . . . . 8 ⊢ ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) → (((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})) → 𝐴 = 𝐶))
71	70	impcom 408	. . . . . . 7 ⊢ ((((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})) ∧ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) → 𝐴 = 𝐶)
72		simpr 485	. . . . . . . 8 ⊢ ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) → 𝐸 = {𝐴})
73	72	adantl 482	. . . . . . 7 ⊢ ((((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})) ∧ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) → 𝐸 = {𝐴})
74	71, 73	jca 516	. . . . . 6 ⊢ ((((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})) ∧ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴}))
75		simpl 483	. . . . . . . . . . 11 ⊢ ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) → 𝐴 = 𝐵)
76	75	adantr 481	. . . . . . . . . 10 ⊢ (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ (𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷})) → 𝐴 = 𝐵)
77		eqeq1 2744	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐸 = {𝐴} → (𝐸 = {𝐶} ↔ {𝐴} = {𝐶}))
78	1	sneqr 4778	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝐴} = {𝐶} → 𝐴 = 𝐶)
79	78	eqcomd 2746	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝐴} = {𝐶} → 𝐶 = 𝐴)
80	77, 79	biimtrdi 254	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸 = {𝐴} → (𝐸 = {𝐶} → 𝐶 = 𝐴))
81	80	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) → (𝐸 = {𝐶} → 𝐶 = 𝐴))
82	81	impcom 408	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 = {𝐶} ∧ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) → 𝐶 = 𝐴)
83	82	preq1d 4678	. . . . . . . . . . . . . 14 ⊢ ((𝐸 = {𝐶} ∧ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) → {𝐶, 𝐷} = {𝐴, 𝐷})
84	83	eqeq2d 2751	. . . . . . . . . . . . 13 ⊢ ((𝐸 = {𝐶} ∧ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) → (𝐹 = {𝐶, 𝐷} ↔ 𝐹 = {𝐴, 𝐷}))
85	84	biimpd 230	. . . . . . . . . . . 12 ⊢ ((𝐸 = {𝐶} ∧ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) → (𝐹 = {𝐶, 𝐷} → 𝐹 = {𝐴, 𝐷}))
86	85	impancom 452	. . . . . . . . . . 11 ⊢ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) → ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) → 𝐹 = {𝐴, 𝐷}))
87	86	impcom 408	. . . . . . . . . 10 ⊢ (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ (𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷})) → 𝐹 = {𝐴, 𝐷})
88	76, 87	jca 516	. . . . . . . . 9 ⊢ (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ (𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷})) → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}))
89	88	ex 413	. . . . . . . 8 ⊢ ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) → ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷})))
90		eqcom 2747	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 = 𝐴 ↔ 𝐴 = 𝐷)
91	90	bilani 505	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) → 𝐴 = 𝐷)
92	91	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) → 𝐴 = 𝐷)
93	92	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) ∧ 𝐹 = {𝐶}) → 𝐴 = 𝐷)
94		simpr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵)
95	64	eqeq1d 2742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) → (𝐴 = 𝐵 ↔ 𝐶 = 𝐵))
96	95	biimpa 477	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) → 𝐶 = 𝐵)
97	96	eqcomd 2746	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) → 𝐵 = 𝐶)
98	1, 2	preqsn 4800	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶))
99	94, 97, 98	sylanbrc 589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) → {𝐴, 𝐵} = {𝐶})
100	99	eqcomd 2746	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) → {𝐶} = {𝐴, 𝐵})
101	100	eqeq2d 2751	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) → (𝐹 = {𝐶} ↔ 𝐹 = {𝐴, 𝐵}))
102	101	biimpa 477	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) ∧ 𝐹 = {𝐶}) → 𝐹 = {𝐴, 𝐵})
103	93, 102	jca 516	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) ∧ 𝐹 = {𝐶}) → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))
104	103	ex 413	. . . . . . . . . . . . . . . 16 ⊢ (((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) → (𝐹 = {𝐶} → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))
105	104	ex 413	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) → (𝐴 = 𝐵 → (𝐹 = {𝐶} → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))
106	105	com23 86	. . . . . . . . . . . . . 14 ⊢ ((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) → (𝐹 = {𝐶} → (𝐴 = 𝐵 → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))
107	62, 106	sylbi 218	. . . . . . . . . . . . 13 ⊢ ({𝐶, 𝐷} = {𝐴} → (𝐹 = {𝐶} → (𝐴 = 𝐵 → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))
108	61, 107	biimtrdi 254	. . . . . . . . . . . 12 ⊢ (𝐸 = {𝐶, 𝐷} → (𝐸 = {𝐴} → (𝐹 = {𝐶} → (𝐴 = 𝐵 → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))))
109	108	com23 86	. . . . . . . . . . 11 ⊢ (𝐸 = {𝐶, 𝐷} → (𝐹 = {𝐶} → (𝐸 = {𝐴} → (𝐴 = 𝐵 → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))))
110	109	imp 407	. . . . . . . . . 10 ⊢ ((𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}) → (𝐸 = {𝐴} → (𝐴 = 𝐵 → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))
111	110	com13 88	. . . . . . . . 9 ⊢ (𝐴 = 𝐵 → (𝐸 = {𝐴} → ((𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}) → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))
112	111	imp 407	. . . . . . . 8 ⊢ ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) → ((𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}) → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))
113	89, 112	orim12d 972	. . . . . . 7 ⊢ ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) → (((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})) → ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))
114	113	impcom 408	. . . . . 6 ⊢ ((((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})) ∧ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) → ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))
115	74, 114	jca 516	. . . . 5 ⊢ ((((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})) ∧ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))
116	115	ancoms 459	. . . 4 ⊢ (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))
117		eqeq1 2744	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 = {𝐶} → (𝐸 = {𝐴, 𝐵} ↔ {𝐶} = {𝐴, 𝐵}))
118		eqcom 2747	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝐶} = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = {𝐶})
119	118, 98	bitri 276	. . . . . . . . . . . . . . . . 17 ⊢ ({𝐶} = {𝐴, 𝐵} ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶))
120		eqtr 2760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)
121	120	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐸 = {𝐶}) → 𝐴 = 𝐶)
122	120	eqcomd 2746	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐶 = 𝐴)
123		sneq 4572	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐶 = 𝐴 → {𝐶} = {𝐴})
124	122, 123	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → {𝐶} = {𝐴})
125	124	eqeq2d 2751	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐸 = {𝐶} ↔ 𝐸 = {𝐴}))
126	125	biimpa 477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐸 = {𝐶}) → 𝐸 = {𝐴})
127	121, 126	jca 516	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐸 = {𝐶}) → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴}))
128	127	ex 413	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐸 = {𝐶} → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})))
129	128	a1i13 27	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶 = 𝐷 → ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐹 = {𝐴} → (𝐸 = {𝐶} → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})))))
130	129	com14 96	. . . . . . . . . . . . . . . . 17 ⊢ (𝐸 = {𝐶} → ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐹 = {𝐴} → (𝐶 = 𝐷 → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})))))
131	119, 130	biimtrid 243	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 = {𝐶} → ({𝐶} = {𝐴, 𝐵} → (𝐹 = {𝐴} → (𝐶 = 𝐷 → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})))))
132	117, 131	sylbid 241	. . . . . . . . . . . . . . 15 ⊢ (𝐸 = {𝐶} → (𝐸 = {𝐴, 𝐵} → (𝐹 = {𝐴} → (𝐶 = 𝐷 → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})))))
133	132	com24 95	. . . . . . . . . . . . . 14 ⊢ (𝐸 = {𝐶} → (𝐶 = 𝐷 → (𝐹 = {𝐴} → (𝐸 = {𝐴, 𝐵} → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})))))
134	133	impcom 408	. . . . . . . . . . . . 13 ⊢ ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → (𝐹 = {𝐴} → (𝐸 = {𝐴, 𝐵} → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴}))))
135	134	com13 88	. . . . . . . . . . . 12 ⊢ (𝐸 = {𝐴, 𝐵} → (𝐹 = {𝐴} → ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴}))))
136	135	imp 407	. . . . . . . . . . 11 ⊢ ((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) → ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})))
137	59	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → (𝐸 = {𝐴} → 𝐴 = 𝐶))
138	137	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝐸 = {𝐴} → ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → 𝐴 = 𝐶))
139	138	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) → ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → 𝐴 = 𝐶))
140	139	imp 407	. . . . . . . . . . . . 13 ⊢ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})) → 𝐴 = 𝐶)
141		simpl 483	. . . . . . . . . . . . . 14 ⊢ ((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) → 𝐸 = {𝐴})
142	141	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})) → 𝐸 = {𝐴})
143	140, 142	jca 516	. . . . . . . . . . . 12 ⊢ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})) → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴}))
144	143	ex 413	. . . . . . . . . . 11 ⊢ ((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) → ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})))
145	136, 144	jaoi 863	. . . . . . . . . 10 ⊢ (((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) ∨ (𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵})) → ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})))
146	145	impcom 408	. . . . . . . . 9 ⊢ (((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) ∧ ((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) ∨ (𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}))) → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴}))
147		eqeq1 2744	. . . . . . . . . . . . . . . 16 ⊢ (𝐸 = {𝐴, 𝐵} → (𝐸 = {𝐶} ↔ {𝐴, 𝐵} = {𝐶}))
148		simpl 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)
149	148	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐶 = 𝐷) → 𝐴 = 𝐵)
150	149	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐶 = 𝐷) ∧ 𝐹 = {𝐴}) → 𝐴 = 𝐵)
151		eqtr 2760	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐴 = 𝐶 ∧ 𝐶 = 𝐷) → 𝐴 = 𝐷)
152		dfsn2 4575	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ {𝐴} = {𝐴, 𝐴}
153		preq2 4673	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴 = 𝐷 → {𝐴, 𝐴} = {𝐴, 𝐷})
154	152, 153	eqtrid 2787	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 = 𝐷 → {𝐴} = {𝐴, 𝐷})
155	151, 154	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴 = 𝐶 ∧ 𝐶 = 𝐷) → {𝐴} = {𝐴, 𝐷})
156	155	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 = 𝐶 → (𝐶 = 𝐷 → {𝐴} = {𝐴, 𝐷}))
157	120, 156	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐶 = 𝐷 → {𝐴} = {𝐴, 𝐷}))
158	157	imp 407	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐶 = 𝐷) → {𝐴} = {𝐴, 𝐷})
159	158	eqeq2d 2751	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐶 = 𝐷) → (𝐹 = {𝐴} ↔ 𝐹 = {𝐴, 𝐷}))
160	159	biimpa 477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐶 = 𝐷) ∧ 𝐹 = {𝐴}) → 𝐹 = {𝐴, 𝐷})
161	150, 160	jca 516	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐶 = 𝐷) ∧ 𝐹 = {𝐴}) → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}))
162	161	ex 413	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐶 = 𝐷) → (𝐹 = {𝐴} → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷})))
163	162	ex 413	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐶 = 𝐷 → (𝐹 = {𝐴} → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}))))
164	163	com23 86	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐹 = {𝐴} → (𝐶 = 𝐷 → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}))))
165	98, 164	sylbi 218	. . . . . . . . . . . . . . . 16 ⊢ ({𝐴, 𝐵} = {𝐶} → (𝐹 = {𝐴} → (𝐶 = 𝐷 → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}))))
166	147, 165	biimtrdi 254	. . . . . . . . . . . . . . 15 ⊢ (𝐸 = {𝐴, 𝐵} → (𝐸 = {𝐶} → (𝐹 = {𝐴} → (𝐶 = 𝐷 → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷})))))
167	166	com23 86	. . . . . . . . . . . . . 14 ⊢ (𝐸 = {𝐴, 𝐵} → (𝐹 = {𝐴} → (𝐸 = {𝐶} → (𝐶 = 𝐷 → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷})))))
168	167	imp 407	. . . . . . . . . . . . 13 ⊢ ((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) → (𝐸 = {𝐶} → (𝐶 = 𝐷 → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}))))
169	168	com13 88	. . . . . . . . . . . 12 ⊢ (𝐶 = 𝐷 → (𝐸 = {𝐶} → ((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}))))
170	169	imp 407	. . . . . . . . . . 11 ⊢ ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → ((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷})))
171	80	imp 407	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐸 = {𝐴} ∧ 𝐸 = {𝐶}) → 𝐶 = 𝐴)
172	171	eqeq1d 2742	. . . . . . . . . . . . . . . 16 ⊢ ((𝐸 = {𝐴} ∧ 𝐸 = {𝐶}) → (𝐶 = 𝐷 ↔ 𝐴 = 𝐷))
173	172	biimpd 230	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 = {𝐴} ∧ 𝐸 = {𝐶}) → (𝐶 = 𝐷 → 𝐴 = 𝐷))
174	173	ex 413	. . . . . . . . . . . . . 14 ⊢ (𝐸 = {𝐴} → (𝐸 = {𝐶} → (𝐶 = 𝐷 → 𝐴 = 𝐷)))
175	174	com13 88	. . . . . . . . . . . . 13 ⊢ (𝐶 = 𝐷 → (𝐸 = {𝐶} → (𝐸 = {𝐴} → 𝐴 = 𝐷)))
176	175	imp 407	. . . . . . . . . . . 12 ⊢ ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → (𝐸 = {𝐴} → 𝐴 = 𝐷))
177	176	anim1d 617	. . . . . . . . . . 11 ⊢ ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → ((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))
178	170, 177	orim12d 972	. . . . . . . . . 10 ⊢ ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → (((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) ∨ (𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵})) → ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))
179	178	imp 407	. . . . . . . . 9 ⊢ (((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) ∧ ((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) ∨ (𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}))) → ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))
180	146, 179	jca 516	. . . . . . . 8 ⊢ (((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) ∧ ((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) ∨ (𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}))) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))
181	180	ex 413	. . . . . . 7 ⊢ ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → (((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) ∨ (𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵})) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))))
182	181	com12 32	. . . . . 6 ⊢ (((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) ∨ (𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵})) → ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))))
183	182	orcoms 878	. . . . 5 ⊢ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) → ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))))
184	183	imp 407	. . . 4 ⊢ ((((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))
185	116, 184	jaoi 863	. . 3 ⊢ ((((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) ∨ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶}))) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))
186	55, 185	impbii 210	. 2 ⊢ (((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))) ↔ (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) ∨ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶}))))
187	13, 18, 186	3bitr4i 304	1 ⊢ ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ⟨𝐸, 𝐹⟩ ↔ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853   = wceq 1547   ∈ wcel 2119  Vcvv 3432  {csn 4562  {cpr 4564  ⟨cop 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569

This theorem is referenced by:  propssopi  5456  fun2dmnopgexmpl  47754