snopeqop

Description: Equivalence for an ordered pair equal to a singleton of an ordered pair. (Contributed by AV, 18-Sep-2020) (Revised by AV, 15-Jul-2022) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	snopeqop.a	$⊢ A \in V$
	snopeqop.b	$⊢ B \in V$
Assertion	snopeqop	$⊢ \{⟨A, B⟩\} = ⟨C, D⟩ \leftrightarrow (A = B \land C = D \land C = \{A\})$

Proof

Step	Hyp	Ref	Expression
1		snopeqop.a	$⊢ A \in V$
2		snopeqop.b	$⊢ B \in V$
3		eqcom	$⊢ \{⟨A, B⟩\} = ⟨C, D⟩ \leftrightarrow ⟨C, D⟩ = \{⟨A, B⟩\}$
4		opeqsng	$⊢ (C \in V \land D \in V) \to (⟨C, D⟩ = \{⟨A, B⟩\} \leftrightarrow (C = D \land ⟨A, B⟩ = \{C\}))$
5	4	ancoms	$⊢ (D \in V \land C \in V) \to (⟨C, D⟩ = \{⟨A, B⟩\} \leftrightarrow (C = D \land ⟨A, B⟩ = \{C\}))$
6	3 5	syl5bb	$⊢ (D \in V \land C \in V) \to (\{⟨A, B⟩\} = ⟨C, D⟩ \leftrightarrow (C = D \land ⟨A, B⟩ = \{C\}))$
7	1 2	opeqsn	$⊢ ⟨A, B⟩ = \{C\} \leftrightarrow (A = B \land C = \{A\})$
8	7	a1i	$⊢ (D \in V \land C \in V) \to (⟨A, B⟩ = \{C\} \leftrightarrow (A = B \land C = \{A\}))$
9	8	anbi2d	$⊢ (D \in V \land C \in V) \to ((C = D \land ⟨A, B⟩ = \{C\}) \leftrightarrow (C = D \land (A = B \land C = \{A\})))$
10		3anan12	$⊢ (A = B \land C = D \land C = \{A\}) \leftrightarrow (C = D \land (A = B \land C = \{A\}))$
11	10	bicomi	$⊢ (C = D \land (A = B \land C = \{A\})) \leftrightarrow (A = B \land C = D \land C = \{A\})$
12	11	a1i	$⊢ (D \in V \land C \in V) \to ((C = D \land (A = B \land C = \{A\})) \leftrightarrow (A = B \land C = D \land C = \{A\}))$
13	6 9 12	3bitrd	$⊢ (D \in V \land C \in V) \to (\{⟨A, B⟩\} = ⟨C, D⟩ \leftrightarrow (A = B \land C = D \land C = \{A\}))$
14		opprc2	$⊢ \neg D \in V \to ⟨C, D⟩ = \emptyset$
15	14	eqeq2d	$⊢ \neg D \in V \to (\{⟨A, B⟩\} = ⟨C, D⟩ \leftrightarrow \{⟨A, B⟩\} = \emptyset)$
16		opex	$⊢ ⟨A, B⟩ \in V$
17	16	snnz	$⊢ \{⟨A, B⟩\} \neq \emptyset$
18		eqneqall	$⊢ \{⟨A, B⟩\} = \emptyset \to (\{⟨A, B⟩\} \neq \emptyset \to (A = B \land C = D \land C = \{A\}))$
19	17 18	mpi	$⊢ \{⟨A, B⟩\} = \emptyset \to (A = B \land C = D \land C = \{A\})$
20	15 19	syl6bi	$⊢ \neg D \in V \to (\{⟨A, B⟩\} = ⟨C, D⟩ \to (A = B \land C = D \land C = \{A\}))$
21	20	adantr	$⊢ (\neg D \in V \land C \in V) \to (\{⟨A, B⟩\} = ⟨C, D⟩ \to (A = B \land C = D \land C = \{A\}))$
22		eleq1	$⊢ D = C \to (D \in V \leftrightarrow C \in V)$
23	22	notbid	$⊢ D = C \to (\neg D \in V \leftrightarrow \neg C \in V)$
24	23	eqcoms	$⊢ C = D \to (\neg D \in V \leftrightarrow \neg C \in V)$
25		pm2.21	$⊢ \neg C \in V \to (C \in V \to \{⟨A, B⟩\} = ⟨C, D⟩)$
26	24 25	syl6bi	$⊢ C = D \to (\neg D \in V \to (C \in V \to \{⟨A, B⟩\} = ⟨C, D⟩))$
27	26	impd	$⊢ C = D \to ((\neg D \in V \land C \in V) \to \{⟨A, B⟩\} = ⟨C, D⟩)$
28	27	3ad2ant2	$⊢ (A = B \land C = D \land C = \{A\}) \to ((\neg D \in V \land C \in V) \to \{⟨A, B⟩\} = ⟨C, D⟩)$
29	28	com12	$⊢ (\neg D \in V \land C \in V) \to ((A = B \land C = D \land C = \{A\}) \to \{⟨A, B⟩\} = ⟨C, D⟩)$
30	21 29	impbid	$⊢ (\neg D \in V \land C \in V) \to (\{⟨A, B⟩\} = ⟨C, D⟩ \leftrightarrow (A = B \land C = D \land C = \{A\}))$
31	13 30	pm2.61ian	$⊢ C \in V \to (\{⟨A, B⟩\} = ⟨C, D⟩ \leftrightarrow (A = B \land C = D \land C = \{A\}))$
32		opprc1	$⊢ \neg C \in V \to ⟨C, D⟩ = \emptyset$
33	32	eqeq2d	$⊢ \neg C \in V \to (\{⟨A, B⟩\} = ⟨C, D⟩ \leftrightarrow \{⟨A, B⟩\} = \emptyset)$
34	33 19	syl6bi	$⊢ \neg C \in V \to (\{⟨A, B⟩\} = ⟨C, D⟩ \to (A = B \land C = D \land C = \{A\}))$
35		eleq1	$⊢ C = \{A\} \to (C \in V \leftrightarrow \{A\} \in V)$
36	35	notbid	$⊢ C = \{A\} \to (\neg C \in V \leftrightarrow \neg \{A\} \in V)$
37		snex	$⊢ \{A\} \in V$
38	37	pm2.24i	$⊢ \neg \{A\} \in V \to \{⟨A, B⟩\} = ⟨C, D⟩$
39	36 38	syl6bi	$⊢ C = \{A\} \to (\neg C \in V \to \{⟨A, B⟩\} = ⟨C, D⟩)$
40	39	3ad2ant3	$⊢ (A = B \land C = D \land C = \{A\}) \to (\neg C \in V \to \{⟨A, B⟩\} = ⟨C, D⟩)$
41	40	com12	$⊢ \neg C \in V \to ((A = B \land C = D \land C = \{A\}) \to \{⟨A, B⟩\} = ⟨C, D⟩)$
42	34 41	impbid	$⊢ \neg C \in V \to (\{⟨A, B⟩\} = ⟨C, D⟩ \leftrightarrow (A = B \land C = D \land C = \{A\}))$
43	31 42	pm2.61i	$⊢ \{⟨A, B⟩\} = ⟨C, D⟩ \leftrightarrow (A = B \land C = D \land C = \{A\})$

Metamath Proof Explorer

Theorem snopeqop

Proof