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 V$
	snopeqop.b	$⊢ B \in V$
	propeqop.c	$⊢ C \in V$
	propeqop.d	$⊢ D \in V$
	propeqop.e	$⊢ E \in V$
	propeqop.f	$⊢ F \in V$
Assertion	propeqop	$⊢ \{⟨A, B⟩, ⟨C, D⟩\} = ⟨E, F⟩ \leftrightarrow ((A = C \land E = \{A\}) \land ((A = B \land F = \{A, D\}) \lor (A = D \land F = \{A, B\})))$

Proof

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

Metamath Proof Explorer

Theorem propeqop

Proof