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	biimtrdi	$⊢ 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	biimtrdi	$⊢ 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	biimtrdi	$⊢ 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	bilani	$⊢ (C = D \land D = A) \to A = D$
92	91	adantr	$⊢ ((C = D \land D = A) \land A = B) \to A = D$
93	92	adantr	$⊢ (((C = D \land D = A) \land A = B) \land F = \{C\}) \to A = D$
94		simpr	$⊢ ((C = D \land D = A) \land A = B) \to A = B$
95	64	eqeq1d	$⊢ (C = D \land D = A) \to (A = B \leftrightarrow C = B)$
96	95	biimpa	$⊢ ((C = D \land D = A) \land A = B) \to C = B$
97	96	eqcomd	$⊢ ((C = D \land D = A) \land A = B) \to B = C$
98	1 2	preqsn	$⊢ \{A, B\} = \{C\} \leftrightarrow (A = B \land B = C)$
99	94 97 98	sylanbrc	$⊢ ((C = D \land D = A) \land A = B) \to \{A, B\} = \{C\}$
100	99	eqcomd	$⊢ ((C = D \land D = A) \land A = B) \to \{C\} = \{A, B\}$
101	100	eqeq2d	$⊢ ((C = D \land D = A) \land A = B) \to (F = \{C\} \leftrightarrow F = \{A, B\})$
102	101	biimpa	$⊢ (((C = D \land D = A) \land A = B) \land F = \{C\}) \to F = \{A, B\}$
103	93 102	jca	$⊢ (((C = D \land D = A) \land A = B) \land F = \{C\}) \to (A = D \land F = \{A, B\})$
104	103	ex	$⊢ ((C = D \land D = A) \land A = B) \to (F = \{C\} \to (A = D \land F = \{A, B\}))$
105	104	ex	$⊢ (C = D \land D = A) \to (A = B \to (F = \{C\} \to (A = D \land F = \{A, B\})))$
106	105	com23	$⊢ (C = D \land D = A) \to (F = \{C\} \to (A = B \to (A = D \land F = \{A, B\})))$
107	62 106	sylbi	$⊢ \{C, D\} = \{A\} \to (F = \{C\} \to (A = B \to (A = D \land F = \{A, B\})))$
108	61 107	biimtrdi	$⊢ E = \{C, D\} \to (E = \{A\} \to (F = \{C\} \to (A = B \to (A = D \land F = \{A, B\}))))$
109	108	com23	$⊢ E = \{C, D\} \to (F = \{C\} \to (E = \{A\} \to (A = B \to (A = D \land F = \{A, B\}))))$
110	109	imp	$⊢ (E = \{C, D\} \land F = \{C\}) \to (E = \{A\} \to (A = B \to (A = D \land F = \{A, B\})))$
111	110	com13	$⊢ A = B \to (E = \{A\} \to ((E = \{C, D\} \land F = \{C\}) \to (A = D \land F = \{A, B\})))$
112	111	imp	$⊢ (A = B \land E = \{A\}) \to ((E = \{C, D\} \land F = \{C\}) \to (A = D \land F = \{A, B\}))$
113	89 112	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\})))$
114	113	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\}))$
115	74 114	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\})))$
116	115	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\})))$
117		eqeq1	$⊢ E = \{C\} \to (E = \{A, B\} \leftrightarrow \{C\} = \{A, B\})$
118		eqcom	$⊢ \{C\} = \{A, B\} \leftrightarrow \{A, B\} = \{C\}$
119	118 98	bitri	$⊢ \{C\} = \{A, B\} \leftrightarrow (A = B \land B = C)$
120		eqtr	$⊢ (A = B \land B = C) \to A = C$
121	120	adantr	$⊢ ((A = B \land B = C) \land E = \{C\}) \to A = C$
122	120	eqcomd	$⊢ (A = B \land B = C) \to C = A$
123		sneq	$⊢ C = A \to \{C\} = \{A\}$
124	122 123	syl	$⊢ (A = B \land B = C) \to \{C\} = \{A\}$
125	124	eqeq2d	$⊢ (A = B \land B = C) \to (E = \{C\} \leftrightarrow E = \{A\})$
126	125	biimpa	$⊢ ((A = B \land B = C) \land E = \{C\}) \to E = \{A\}$
127	121 126	jca	$⊢ ((A = B \land B = C) \land E = \{C\}) \to (A = C \land E = \{A\})$
128	127	ex	$⊢ (A = B \land B = C) \to (E = \{C\} \to (A = C \land E = \{A\}))$
129	128	a1i13	$⊢ C = D \to ((A = B \land B = C) \to (F = \{A\} \to (E = \{C\} \to (A = C \land E = \{A\}))))$
130	129	com14	$⊢ E = \{C\} \to ((A = B \land B = C) \to (F = \{A\} \to (C = D \to (A = C \land E = \{A\}))))$
131	119 130	biimtrid	$⊢ E = \{C\} \to (\{C\} = \{A, B\} \to (F = \{A\} \to (C = D \to (A = C \land E = \{A\}))))$
132	117 131	sylbid	$⊢ E = \{C\} \to (E = \{A, B\} \to (F = \{A\} \to (C = D \to (A = C \land E = \{A\}))))$
133	132	com24	$⊢ E = \{C\} \to (C = D \to (F = \{A\} \to (E = \{A, B\} \to (A = C \land E = \{A\}))))$
134	133	impcom	$⊢ (C = D \land E = \{C\}) \to (F = \{A\} \to (E = \{A, B\} \to (A = C \land E = \{A\})))$
135	134	com13	$⊢ E = \{A, B\} \to (F = \{A\} \to ((C = D \land E = \{C\}) \to (A = C \land E = \{A\})))$
136	135	imp	$⊢ (E = \{A, B\} \land F = \{A\}) \to ((C = D \land E = \{C\}) \to (A = C \land E = \{A\}))$
137	59	adantl	$⊢ (C = D \land E = \{C\}) \to (E = \{A\} \to A = C)$
138	137	com12	$⊢ E = \{A\} \to ((C = D \land E = \{C\}) \to A = C)$
139	138	adantr	$⊢ (E = \{A\} \land F = \{A, B\}) \to ((C = D \land E = \{C\}) \to A = C)$
140	139	imp	$⊢ ((E = \{A\} \land F = \{A, B\}) \land (C = D \land E = \{C\})) \to A = C$
141		simpl	$⊢ (E = \{A\} \land F = \{A, B\}) \to E = \{A\}$
142	141	adantr	$⊢ ((E = \{A\} \land F = \{A, B\}) \land (C = D \land E = \{C\})) \to E = \{A\}$
143	140 142	jca	$⊢ ((E = \{A\} \land F = \{A, B\}) \land (C = D \land E = \{C\})) \to (A = C \land E = \{A\})$
144	143	ex	$⊢ (E = \{A\} \land F = \{A, B\}) \to ((C = D \land E = \{C\}) \to (A = C \land E = \{A\}))$
145	136 144	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\}))$
146	145	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\})$
147		eqeq1	$⊢ E = \{A, B\} \to (E = \{C\} \leftrightarrow \{A, B\} = \{C\})$
148		simpl	$⊢ (A = B \land B = C) \to A = B$
149	148	adantr	$⊢ ((A = B \land B = C) \land C = D) \to A = B$
150	149	adantr	$⊢ (((A = B \land B = C) \land C = D) \land F = \{A\}) \to A = B$
151		eqtr	$⊢ (A = C \land C = D) \to A = D$
152		dfsn2	$⊢ \{A\} = \{A, A\}$
153		preq2	$⊢ A = D \to \{A, A\} = \{A, D\}$
154	152 153	eqtrid	$⊢ A = D \to \{A\} = \{A, D\}$
155	151 154	syl	$⊢ (A = C \land C = D) \to \{A\} = \{A, D\}$
156	155	ex	$⊢ A = C \to (C = D \to \{A\} = \{A, D\})$
157	120 156	syl	$⊢ (A = B \land B = C) \to (C = D \to \{A\} = \{A, D\})$
158	157	imp	$⊢ ((A = B \land B = C) \land C = D) \to \{A\} = \{A, D\}$
159	158	eqeq2d	$⊢ ((A = B \land B = C) \land C = D) \to (F = \{A\} \leftrightarrow F = \{A, D\})$
160	159	biimpa	$⊢ (((A = B \land B = C) \land C = D) \land F = \{A\}) \to F = \{A, D\}$
161	150 160	jca	$⊢ (((A = B \land B = C) \land C = D) \land F = \{A\}) \to (A = B \land F = \{A, D\})$
162	161	ex	$⊢ ((A = B \land B = C) \land C = D) \to (F = \{A\} \to (A = B \land F = \{A, D\}))$
163	162	ex	$⊢ (A = B \land B = C) \to (C = D \to (F = \{A\} \to (A = B \land F = \{A, D\})))$
164	163	com23	$⊢ (A = B \land B = C) \to (F = \{A\} \to (C = D \to (A = B \land F = \{A, D\})))$
165	98 164	sylbi	$⊢ \{A, B\} = \{C\} \to (F = \{A\} \to (C = D \to (A = B \land F = \{A, D\})))$
166	147 165	biimtrdi	$⊢ E = \{A, B\} \to (E = \{C\} \to (F = \{A\} \to (C = D \to (A = B \land F = \{A, D\}))))$
167	166	com23	$⊢ E = \{A, B\} \to (F = \{A\} \to (E = \{C\} \to (C = D \to (A = B \land F = \{A, D\}))))$
168	167	imp	$⊢ (E = \{A, B\} \land F = \{A\}) \to (E = \{C\} \to (C = D \to (A = B \land F = \{A, D\})))$
169	168	com13	$⊢ C = D \to (E = \{C\} \to ((E = \{A, B\} \land F = \{A\}) \to (A = B \land F = \{A, D\})))$
170	169	imp	$⊢ (C = D \land E = \{C\}) \to ((E = \{A, B\} \land F = \{A\}) \to (A = B \land F = \{A, D\}))$
171	80	imp	$⊢ (E = \{A\} \land E = \{C\}) \to C = A$
172	171	eqeq1d	$⊢ (E = \{A\} \land E = \{C\}) \to (C = D \leftrightarrow A = D)$
173	172	biimpd	$⊢ (E = \{A\} \land E = \{C\}) \to (C = D \to A = D)$
174	173	ex	$⊢ E = \{A\} \to (E = \{C\} \to (C = D \to A = D))$
175	174	com13	$⊢ C = D \to (E = \{C\} \to (E = \{A\} \to A = D))$
176	175	imp	$⊢ (C = D \land E = \{C\}) \to (E = \{A\} \to A = D)$
177	176	anim1d	$⊢ (C = D \land E = \{C\}) \to ((E = \{A\} \land F = \{A, B\}) \to (A = D \land F = \{A, B\}))$
178	170 177	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\})))$
179	178	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\}))$
180	146 179	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\})))$
181	180	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\}))))$
182	181	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\}))))$
183	182	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\}))))$
184	183	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\})))$
185	116 184	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\})))$
186	55 185	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\})))$
187	13 18 186	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