euoreqb

Description: There is a set which is equal to one of two other sets iff the other sets are equal. (Contributed by AV, 24-Jan-2023)

		Ref	Expression
	Assertion	euoreqb	$⊢ (A \in V \land B \in V) \to (\exists! x \in V (x = A \lor x = B) \leftrightarrow A = B)$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$⊢ x = y \to (x = A \leftrightarrow y = A)$
2		eqeq1	$⊢ x = y \to (x = B \leftrightarrow y = B)$
3	1 2	orbi12d	$⊢ x = y \to ((x = A \lor x = B) \leftrightarrow (y = A \lor y = B))$
4	3	reu8	$⊢ \exists! x \in V (x = A \lor x = B) \leftrightarrow \exists x \in V ((x = A \lor x = B) \land \forall y \in V ((y = A \lor y = B) \to x = y))$
5		simprlr	$⊢ (x = A \land ((A \in V \land B \in V) \land x \in V)) \to B \in V$
6		eqeq1	$⊢ y = B \to (y = A \leftrightarrow B = A)$
7		eqeq1	$⊢ y = B \to (y = B \leftrightarrow B = B)$
8	6 7	orbi12d	$⊢ y = B \to ((y = A \lor y = B) \leftrightarrow (B = A \lor B = B))$
9		eqeq2	$⊢ y = B \to (x = y \leftrightarrow x = B)$
10	8 9	imbi12d	$⊢ y = B \to (((y = A \lor y = B) \to x = y) \leftrightarrow ((B = A \lor B = B) \to x = B))$
11	10	rspcv	$⊢ B \in V \to (\forall y \in V ((y = A \lor y = B) \to x = y) \to ((B = A \lor B = B) \to x = B))$
12	5 11	syl	$⊢ (x = A \land ((A \in V \land B \in V) \land x \in V)) \to (\forall y \in V ((y = A \lor y = B) \to x = y) \to ((B = A \lor B = B) \to x = B))$
13		ioran	$⊢ \neg (B = A \lor B = B) \leftrightarrow (\neg B = A \land \neg B = B)$
14		eqid	$⊢ B = B$
15	14	pm2.24i	$⊢ \neg B = B \to ((x = A \land ((A \in V \land B \in V) \land x \in V)) \to A = B)$
16	13 15	simplbiim	$⊢ \neg (B = A \lor B = B) \to ((x = A \land ((A \in V \land B \in V) \land x \in V)) \to A = B)$
17		eqtr2	$⊢ (x = A \land x = B) \to A = B$
18	17	ancoms	$⊢ (x = B \land x = A) \to A = B$
19	18	a1d	$⊢ (x = B \land x = A) \to (((A \in V \land B \in V) \land x \in V) \to A = B)$
20	19	expimpd	$⊢ x = B \to ((x = A \land ((A \in V \land B \in V) \land x \in V)) \to A = B)$
21	16 20	ja	$⊢ ((B = A \lor B = B) \to x = B) \to ((x = A \land ((A \in V \land B \in V) \land x \in V)) \to A = B)$
22	21	com12	$⊢ (x = A \land ((A \in V \land B \in V) \land x \in V)) \to (((B = A \lor B = B) \to x = B) \to A = B)$
23	12 22	syld	$⊢ (x = A \land ((A \in V \land B \in V) \land x \in V)) \to (\forall y \in V ((y = A \lor y = B) \to x = y) \to A = B)$
24	23	ex	$⊢ x = A \to (((A \in V \land B \in V) \land x \in V) \to (\forall y \in V ((y = A \lor y = B) \to x = y) \to A = B))$
25		simprll	$⊢ (x = B \land ((A \in V \land B \in V) \land x \in V)) \to A \in V$
26		eqeq1	$⊢ y = A \to (y = A \leftrightarrow A = A)$
27		eqeq1	$⊢ y = A \to (y = B \leftrightarrow A = B)$
28	26 27	orbi12d	$⊢ y = A \to ((y = A \lor y = B) \leftrightarrow (A = A \lor A = B))$
29		eqeq2	$⊢ y = A \to (x = y \leftrightarrow x = A)$
30	28 29	imbi12d	$⊢ y = A \to (((y = A \lor y = B) \to x = y) \leftrightarrow ((A = A \lor A = B) \to x = A))$
31	30	rspcv	$⊢ A \in V \to (\forall y \in V ((y = A \lor y = B) \to x = y) \to ((A = A \lor A = B) \to x = A))$
32	25 31	syl	$⊢ (x = B \land ((A \in V \land B \in V) \land x \in V)) \to (\forall y \in V ((y = A \lor y = B) \to x = y) \to ((A = A \lor A = B) \to x = A))$
33		ioran	$⊢ \neg (A = A \lor A = B) \leftrightarrow (\neg A = A \land \neg A = B)$
34		eqid	$⊢ A = A$
35	34	pm2.24i	$⊢ \neg A = A \to ((x = B \land ((A \in V \land B \in V) \land x \in V)) \to A = B)$
36	35	adantr	$⊢ (\neg A = A \land \neg A = B) \to ((x = B \land ((A \in V \land B \in V) \land x \in V)) \to A = B)$
37	33 36	sylbi	$⊢ \neg (A = A \lor A = B) \to ((x = B \land ((A \in V \land B \in V) \land x \in V)) \to A = B)$
38	17	a1d	$⊢ (x = A \land x = B) \to (((A \in V \land B \in V) \land x \in V) \to A = B)$
39	38	expimpd	$⊢ x = A \to ((x = B \land ((A \in V \land B \in V) \land x \in V)) \to A = B)$
40	37 39	ja	$⊢ ((A = A \lor A = B) \to x = A) \to ((x = B \land ((A \in V \land B \in V) \land x \in V)) \to A = B)$
41	40	com12	$⊢ (x = B \land ((A \in V \land B \in V) \land x \in V)) \to (((A = A \lor A = B) \to x = A) \to A = B)$
42	32 41	syld	$⊢ (x = B \land ((A \in V \land B \in V) \land x \in V)) \to (\forall y \in V ((y = A \lor y = B) \to x = y) \to A = B)$
43	42	ex	$⊢ x = B \to (((A \in V \land B \in V) \land x \in V) \to (\forall y \in V ((y = A \lor y = B) \to x = y) \to A = B))$
44	24 43	jaoi	$⊢ (x = A \lor x = B) \to (((A \in V \land B \in V) \land x \in V) \to (\forall y \in V ((y = A \lor y = B) \to x = y) \to A = B))$
45	44	com12	$⊢ ((A \in V \land B \in V) \land x \in V) \to ((x = A \lor x = B) \to (\forall y \in V ((y = A \lor y = B) \to x = y) \to A = B))$
46	45	impd	$⊢ ((A \in V \land B \in V) \land x \in V) \to (((x = A \lor x = B) \land \forall y \in V ((y = A \lor y = B) \to x = y)) \to A = B)$
47	46	rexlimdva	$⊢ (A \in V \land B \in V) \to (\exists x \in V ((x = A \lor x = B) \land \forall y \in V ((y = A \lor y = B) \to x = y)) \to A = B)$
48	4 47	syl5bi	$⊢ (A \in V \land B \in V) \to (\exists! x \in V (x = A \lor x = B) \to A = B)$
49		reueq	$⊢ B \in V \leftrightarrow \exists! x \in V x = B$
50	49	biimpi	$⊢ B \in V \to \exists! x \in V x = B$
51	50	adantl	$⊢ (A \in V \land B \in V) \to \exists! x \in V x = B$
52	51	adantr	$⊢ ((A \in V \land B \in V) \land A = B) \to \exists! x \in V x = B$
53		eqeq2	$⊢ A = B \to (x = A \leftrightarrow x = B)$
54	53	adantl	$⊢ ((A \in V \land B \in V) \land A = B) \to (x = A \leftrightarrow x = B)$
55	54	orbi1d	$⊢ ((A \in V \land B \in V) \land A = B) \to ((x = A \lor x = B) \leftrightarrow (x = B \lor x = B))$
56		oridm	$⊢ (x = B \lor x = B) \leftrightarrow x = B$
57	55 56	bitrdi	$⊢ ((A \in V \land B \in V) \land A = B) \to ((x = A \lor x = B) \leftrightarrow x = B)$
58	57	reubidv	$⊢ ((A \in V \land B \in V) \land A = B) \to (\exists! x \in V (x = A \lor x = B) \leftrightarrow \exists! x \in V x = B)$
59	52 58	mpbird	$⊢ ((A \in V \land B \in V) \land A = B) \to \exists! x \in V (x = A \lor x = B)$
60	59	ex	$⊢ (A \in V \land B \in V) \to (A = B \to \exists! x \in V (x = A \lor x = B))$
61	48 60	impbid	$⊢ (A \in V \land B \in V) \to (\exists! x \in V (x = A \lor x = B) \leftrightarrow A = B)$

Metamath Proof Explorer

Theorem euoreqb

Proof