paireqne

Description: Two sets are not equal iff there is exactly one proper pair whose elements are either one of these sets. (Contributed by AV, 27-Jan-2023)

	Ref	Expression
Hypotheses	paireqne.a	$⊢ φ \to A \in V$
	paireqne.b	$⊢ φ \to B \in V$
	paireqne.p	$⊢ P = \{x \in 𝒫 V \| \|x\| = 2\}$
Assertion	paireqne	$⊢ φ \to (\exists! p \in P \forall x \in p (x = A \lor x = B) \leftrightarrow A \neq B)$

Proof

Step	Hyp	Ref	Expression
1		paireqne.a	$⊢ φ \to A \in V$
2		paireqne.b	$⊢ φ \to B \in V$
3		paireqne.p	$⊢ P = \{x \in 𝒫 V \| \|x\| = 2\}$
4		raleq	$⊢ p = q \to (\forall x \in p (x = A \lor x = B) \leftrightarrow \forall x \in q (x = A \lor x = B))$
5	4	reu8	$⊢ \exists! p \in P \forall x \in p (x = A \lor x = B) \leftrightarrow \exists p \in P (\forall x \in p (x = A \lor x = B) \land \forall q \in P (\forall x \in q (x = A \lor x = B) \to p = q))$
6	3	eleq2i	$⊢ p \in P \leftrightarrow p \in \{x \in 𝒫 V \| \|x\| = 2\}$
7		elss2prb	$⊢ p \in \{x \in 𝒫 V \| \|x\| = 2\} \leftrightarrow \exists a \in V \exists b \in V (a \neq b \land p = \{a, b\})$
8	6 7	bitri	$⊢ p \in P \leftrightarrow \exists a \in V \exists b \in V (a \neq b \land p = \{a, b\})$
9		raleq	$⊢ p = \{a, b\} \to (\forall x \in p (x = A \lor x = B) \leftrightarrow \forall x \in \{a, b\} (x = A \lor x = B))$
10		vex	$⊢ a \in V$
11		vex	$⊢ b \in V$
12		eqeq1	$⊢ x = a \to (x = A \leftrightarrow a = A)$
13		eqeq1	$⊢ x = a \to (x = B \leftrightarrow a = B)$
14	12 13	orbi12d	$⊢ x = a \to ((x = A \lor x = B) \leftrightarrow (a = A \lor a = B))$
15		eqeq1	$⊢ x = b \to (x = A \leftrightarrow b = A)$
16		eqeq1	$⊢ x = b \to (x = B \leftrightarrow b = B)$
17	15 16	orbi12d	$⊢ x = b \to ((x = A \lor x = B) \leftrightarrow (b = A \lor b = B))$
18	10 11 14 17	ralpr	$⊢ \forall x \in \{a, b\} (x = A \lor x = B) \leftrightarrow ((a = A \lor a = B) \land (b = A \lor b = B))$
19	9 18	syl6bb	$⊢ p = \{a, b\} \to (\forall x \in p (x = A \lor x = B) \leftrightarrow ((a = A \lor a = B) \land (b = A \lor b = B)))$
20		eqeq1	$⊢ p = \{a, b\} \to (p = q \leftrightarrow \{a, b\} = q)$
21	20	imbi2d	$⊢ p = \{a, b\} \to ((\forall x \in q (x = A \lor x = B) \to p = q) \leftrightarrow (\forall x \in q (x = A \lor x = B) \to \{a, b\} = q))$
22	21	ralbidv	$⊢ p = \{a, b\} \to (\forall q \in P (\forall x \in q (x = A \lor x = B) \to p = q) \leftrightarrow \forall q \in P (\forall x \in q (x = A \lor x = B) \to \{a, b\} = q))$
23	19 22	anbi12d	$⊢ p = \{a, b\} \to ((\forall x \in p (x = A \lor x = B) \land \forall q \in P (\forall x \in q (x = A \lor x = B) \to p = q)) \leftrightarrow (((a = A \lor a = B) \land (b = A \lor b = B)) \land \forall q \in P (\forall x \in q (x = A \lor x = B) \to \{a, b\} = q)))$
24	23	ad2antll	$⊢ ((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to ((\forall x \in p (x = A \lor x = B) \land \forall q \in P (\forall x \in q (x = A \lor x = B) \to p = q)) \leftrightarrow (((a = A \lor a = B) \land (b = A \lor b = B)) \land \forall q \in P (\forall x \in q (x = A \lor x = B) \to \{a, b\} = q)))$
25	1 2	jca	$⊢ φ \to (A \in V \land B \in V)$
26		prelpwi	$⊢ (A \in V \land B \in V) \to \{A, B\} \in 𝒫 V$
27	25 26	syl	$⊢ φ \to \{A, B\} \in 𝒫 V$
28	27	ad3antrrr	$⊢ (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \land ((a = A \lor a = B) \land (b = A \lor b = B))) \to \{A, B\} \in 𝒫 V$
29		hashprg	$⊢ (a \in V \land b \in V) \to (a \neq b \leftrightarrow \|\{a, b\}\| = 2)$
30	29	adantl	$⊢ (φ \land (a \in V \land b \in V)) \to (a \neq b \leftrightarrow \|\{a, b\}\| = 2)$
31	30	biimpd	$⊢ (φ \land (a \in V \land b \in V)) \to (a \neq b \to \|\{a, b\}\| = 2)$
32	31	com12	$⊢ a \neq b \to ((φ \land (a \in V \land b \in V)) \to \|\{a, b\}\| = 2)$
33	32	adantr	$⊢ (a \neq b \land p = \{a, b\}) \to ((φ \land (a \in V \land b \in V)) \to \|\{a, b\}\| = 2)$
34	33	impcom	$⊢ ((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to \|\{a, b\}\| = 2$
35	34	adantr	$⊢ (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \land ((a = A \lor a = B) \land (b = A \lor b = B))) \to \|\{a, b\}\| = 2$
36		eqtr3	$⊢ (b = A \land a = A) \to b = a$
37		eqneqall	$⊢ a = b \to (a \neq b \to (p = \{a, b\} \to \{A, B\} = \{a, b\}))$
38	37	impd	$⊢ a = b \to ((a \neq b \land p = \{a, b\}) \to \{A, B\} = \{a, b\})$
39	38	a1d	$⊢ a = b \to ((φ \land (a \in V \land b \in V)) \to ((a \neq b \land p = \{a, b\}) \to \{A, B\} = \{a, b\}))$
40	39	impd	$⊢ a = b \to (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to \{A, B\} = \{a, b\})$
41	40	equcoms	$⊢ b = a \to (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to \{A, B\} = \{a, b\})$
42	36 41	syl	$⊢ (b = A \land a = A) \to (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to \{A, B\} = \{a, b\})$
43	42	ex	$⊢ b = A \to (a = A \to (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to \{A, B\} = \{a, b\}))$
44		preq12	$⊢ (a = A \land b = B) \to \{a, b\} = \{A, B\}$
45	44	eqcomd	$⊢ (a = A \land b = B) \to \{A, B\} = \{a, b\}$
46	45	a1d	$⊢ (a = A \land b = B) \to (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to \{A, B\} = \{a, b\})$
47	46	expcom	$⊢ b = B \to (a = A \to (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to \{A, B\} = \{a, b\}))$
48	43 47	jaoi	$⊢ (b = A \lor b = B) \to (a = A \to (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to \{A, B\} = \{a, b\}))$
49	48	com12	$⊢ a = A \to ((b = A \lor b = B) \to (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to \{A, B\} = \{a, b\}))$
50		prcom	$⊢ \{a, b\} = \{b, a\}$
51		preq12	$⊢ (b = A \land a = B) \to \{b, a\} = \{A, B\}$
52	50 51	syl5eq	$⊢ (b = A \land a = B) \to \{a, b\} = \{A, B\}$
53	52	eqcomd	$⊢ (b = A \land a = B) \to \{A, B\} = \{a, b\}$
54	53	a1d	$⊢ (b = A \land a = B) \to (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to \{A, B\} = \{a, b\})$
55	54	ex	$⊢ b = A \to (a = B \to (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to \{A, B\} = \{a, b\}))$
56		eqtr3	$⊢ (b = B \land a = B) \to b = a$
57	56 41	syl	$⊢ (b = B \land a = B) \to (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to \{A, B\} = \{a, b\})$
58	57	ex	$⊢ b = B \to (a = B \to (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to \{A, B\} = \{a, b\}))$
59	55 58	jaoi	$⊢ (b = A \lor b = B) \to (a = B \to (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to \{A, B\} = \{a, b\}))$
60	59	com12	$⊢ a = B \to ((b = A \lor b = B) \to (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to \{A, B\} = \{a, b\}))$
61	49 60	jaoi	$⊢ (a = A \lor a = B) \to ((b = A \lor b = B) \to (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to \{A, B\} = \{a, b\}))$
62	61	imp	$⊢ ((a = A \lor a = B) \land (b = A \lor b = B)) \to (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to \{A, B\} = \{a, b\})$
63	62	impcom	$⊢ (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \land ((a = A \lor a = B) \land (b = A \lor b = B))) \to \{A, B\} = \{a, b\}$
64	63	fveqeq2d	$⊢ (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \land ((a = A \lor a = B) \land (b = A \lor b = B))) \to (\|\{A, B\}\| = 2 \leftrightarrow \|\{a, b\}\| = 2)$
65	35 64	mpbird	$⊢ (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \land ((a = A \lor a = B) \land (b = A \lor b = B))) \to \|\{A, B\}\| = 2$
66	28 65	jca	$⊢ (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \land ((a = A \lor a = B) \land (b = A \lor b = B))) \to (\{A, B\} \in 𝒫 V \land \|\{A, B\}\| = 2)$
67	3	eleq2i	$⊢ \{A, B\} \in P \leftrightarrow \{A, B\} \in \{x \in 𝒫 V \| \|x\| = 2\}$
68		fveqeq2	$⊢ x = \{A, B\} \to (\|x\| = 2 \leftrightarrow \|\{A, B\}\| = 2)$
69	68	elrab	$⊢ \{A, B\} \in \{x \in 𝒫 V \| \|x\| = 2\} \leftrightarrow (\{A, B\} \in 𝒫 V \land \|\{A, B\}\| = 2)$
70	67 69	bitri	$⊢ \{A, B\} \in P \leftrightarrow (\{A, B\} \in 𝒫 V \land \|\{A, B\}\| = 2)$
71	66 70	sylibr	$⊢ (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \land ((a = A \lor a = B) \land (b = A \lor b = B))) \to \{A, B\} \in P$
72		raleq	$⊢ q = \{A, B\} \to (\forall x \in q (x = A \lor x = B) \leftrightarrow \forall x \in \{A, B\} (x = A \lor x = B))$
73		eqeq2	$⊢ q = \{A, B\} \to (\{a, b\} = q \leftrightarrow \{a, b\} = \{A, B\})$
74	72 73	imbi12d	$⊢ q = \{A, B\} \to ((\forall x \in q (x = A \lor x = B) \to \{a, b\} = q) \leftrightarrow (\forall x \in \{A, B\} (x = A \lor x = B) \to \{a, b\} = \{A, B\}))$
75	74	rspcv	$⊢ \{A, B\} \in P \to (\forall q \in P (\forall x \in q (x = A \lor x = B) \to \{a, b\} = q) \to (\forall x \in \{A, B\} (x = A \lor x = B) \to \{a, b\} = \{A, B\}))$
76	71 75	syl	$⊢ (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \land ((a = A \lor a = B) \land (b = A \lor b = B))) \to (\forall q \in P (\forall x \in q (x = A \lor x = B) \to \{a, b\} = q) \to (\forall x \in \{A, B\} (x = A \lor x = B) \to \{a, b\} = \{A, B\}))$
77		eqeq1	$⊢ x = A \to (x = A \leftrightarrow A = A)$
78		eqeq1	$⊢ x = A \to (x = B \leftrightarrow A = B)$
79	77 78	orbi12d	$⊢ x = A \to ((x = A \lor x = B) \leftrightarrow (A = A \lor A = B))$
80		eqeq1	$⊢ x = B \to (x = A \leftrightarrow B = A)$
81		eqeq1	$⊢ x = B \to (x = B \leftrightarrow B = B)$
82	80 81	orbi12d	$⊢ x = B \to ((x = A \lor x = B) \leftrightarrow (B = A \lor B = B))$
83	79 82	ralprg	$⊢ (A \in V \land B \in V) \to (\forall x \in \{A, B\} (x = A \lor x = B) \leftrightarrow ((A = A \lor A = B) \land (B = A \lor B = B)))$
84	25 83	syl	$⊢ φ \to (\forall x \in \{A, B\} (x = A \lor x = B) \leftrightarrow ((A = A \lor A = B) \land (B = A \lor B = B)))$
85	84	imbi1d	$⊢ φ \to ((\forall x \in \{A, B\} (x = A \lor x = B) \to \{a, b\} = \{A, B\}) \leftrightarrow (((A = A \lor A = B) \land (B = A \lor B = B)) \to \{a, b\} = \{A, B\}))$
86	85	ad3antrrr	$⊢ (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \land ((a = A \lor a = B) \land (b = A \lor b = B))) \to ((\forall x \in \{A, B\} (x = A \lor x = B) \to \{a, b\} = \{A, B\}) \leftrightarrow (((A = A \lor A = B) \land (B = A \lor B = B)) \to \{a, b\} = \{A, B\}))$
87		eqid	$⊢ A = A$
88	87	orci	$⊢ (A = A \lor A = B)$
89		eqid	$⊢ B = B$
90	89	olci	$⊢ (B = A \lor B = B)$
91		pm5.5	$⊢ ((A = A \lor A = B) \land (B = A \lor B = B)) \to ((((A = A \lor A = B) \land (B = A \lor B = B)) \to \{a, b\} = \{A, B\}) \leftrightarrow \{a, b\} = \{A, B\})$
92	88 90 91	mp2an	$⊢ (((A = A \lor A = B) \land (B = A \lor B = B)) \to \{a, b\} = \{A, B\}) \leftrightarrow \{a, b\} = \{A, B\}$
93	10 11	pm3.2i	$⊢ (a \in V \land b \in V)$
94		preq12bg	$⊢ ((a \in V \land b \in V) \land (A \in V \land B \in V)) \to (\{a, b\} = \{A, B\} \leftrightarrow ((a = A \land b = B) \lor (a = B \land b = A)))$
95	93 25 94	sylancr	$⊢ φ \to (\{a, b\} = \{A, B\} \leftrightarrow ((a = A \land b = B) \lor (a = B \land b = A)))$
96	95	adantr	$⊢ (φ \land (a \in V \land b \in V)) \to (\{a, b\} = \{A, B\} \leftrightarrow ((a = A \land b = B) \lor (a = B \land b = A)))$
97	96	adantr	$⊢ ((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to (\{a, b\} = \{A, B\} \leftrightarrow ((a = A \land b = B) \lor (a = B \land b = A)))$
98		eqeq12	$⊢ (a = A \land b = B) \to (a = b \leftrightarrow A = B)$
99	98	necon3bid	$⊢ (a = A \land b = B) \to (a \neq b \leftrightarrow A \neq B)$
100	99	biimpd	$⊢ (a = A \land b = B) \to (a \neq b \to A \neq B)$
101		eqeq12	$⊢ (a = B \land b = A) \to (a = b \leftrightarrow B = A)$
102	101	necon3bid	$⊢ (a = B \land b = A) \to (a \neq b \leftrightarrow B \neq A)$
103	102	biimpd	$⊢ (a = B \land b = A) \to (a \neq b \to B \neq A)$
104		necom	$⊢ A \neq B \leftrightarrow B \neq A$
105	103 104	syl6ibr	$⊢ (a = B \land b = A) \to (a \neq b \to A \neq B)$
106	100 105	jaoi	$⊢ ((a = A \land b = B) \lor (a = B \land b = A)) \to (a \neq b \to A \neq B)$
107	106	com12	$⊢ a \neq b \to (((a = A \land b = B) \lor (a = B \land b = A)) \to A \neq B)$
108	107	ad2antrl	$⊢ ((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to (((a = A \land b = B) \lor (a = B \land b = A)) \to A \neq B)$
109	97 108	sylbid	$⊢ ((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to (\{a, b\} = \{A, B\} \to A \neq B)$
110	109	adantr	$⊢ (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \land ((a = A \lor a = B) \land (b = A \lor b = B))) \to (\{a, b\} = \{A, B\} \to A \neq B)$
111	92 110	syl5bi	$⊢ (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \land ((a = A \lor a = B) \land (b = A \lor b = B))) \to ((((A = A \lor A = B) \land (B = A \lor B = B)) \to \{a, b\} = \{A, B\}) \to A \neq B)$
112	86 111	sylbid	$⊢ (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \land ((a = A \lor a = B) \land (b = A \lor b = B))) \to ((\forall x \in \{A, B\} (x = A \lor x = B) \to \{a, b\} = \{A, B\}) \to A \neq B)$
113	76 112	syld	$⊢ (((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \land ((a = A \lor a = B) \land (b = A \lor b = B))) \to (\forall q \in P (\forall x \in q (x = A \lor x = B) \to \{a, b\} = q) \to A \neq B)$
114	113	ex	$⊢ ((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to (((a = A \lor a = B) \land (b = A \lor b = B)) \to (\forall q \in P (\forall x \in q (x = A \lor x = B) \to \{a, b\} = q) \to A \neq B))$
115	114	impd	$⊢ ((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to ((((a = A \lor a = B) \land (b = A \lor b = B)) \land \forall q \in P (\forall x \in q (x = A \lor x = B) \to \{a, b\} = q)) \to A \neq B)$
116	24 115	sylbid	$⊢ ((φ \land (a \in V \land b \in V)) \land (a \neq b \land p = \{a, b\})) \to ((\forall x \in p (x = A \lor x = B) \land \forall q \in P (\forall x \in q (x = A \lor x = B) \to p = q)) \to A \neq B)$
117	116	ex	$⊢ (φ \land (a \in V \land b \in V)) \to ((a \neq b \land p = \{a, b\}) \to ((\forall x \in p (x = A \lor x = B) \land \forall q \in P (\forall x \in q (x = A \lor x = B) \to p = q)) \to A \neq B))$
118	117	rexlimdvva	$⊢ φ \to (\exists a \in V \exists b \in V (a \neq b \land p = \{a, b\}) \to ((\forall x \in p (x = A \lor x = B) \land \forall q \in P (\forall x \in q (x = A \lor x = B) \to p = q)) \to A \neq B))$
119	8 118	syl5bi	$⊢ φ \to (p \in P \to ((\forall x \in p (x = A \lor x = B) \land \forall q \in P (\forall x \in q (x = A \lor x = B) \to p = q)) \to A \neq B))$
120	119	imp	$⊢ (φ \land p \in P) \to ((\forall x \in p (x = A \lor x = B) \land \forall q \in P (\forall x \in q (x = A \lor x = B) \to p = q)) \to A \neq B)$
121	120	rexlimdva	$⊢ φ \to (\exists p \in P (\forall x \in p (x = A \lor x = B) \land \forall q \in P (\forall x \in q (x = A \lor x = B) \to p = q)) \to A \neq B)$
122	5 121	syl5bi	$⊢ φ \to (\exists! p \in P \forall x \in p (x = A \lor x = B) \to A \neq B)$
123	27	adantr	$⊢ (φ \land A \neq B) \to \{A, B\} \in 𝒫 V$
124		hashprg	$⊢ (A \in V \land B \in V) \to (A \neq B \leftrightarrow \|\{A, B\}\| = 2)$
125	25 124	syl	$⊢ φ \to (A \neq B \leftrightarrow \|\{A, B\}\| = 2)$
126	125	biimpd	$⊢ φ \to (A \neq B \to \|\{A, B\}\| = 2)$
127	126	imp	$⊢ (φ \land A \neq B) \to \|\{A, B\}\| = 2$
128	123 127	jca	$⊢ (φ \land A \neq B) \to (\{A, B\} \in 𝒫 V \land \|\{A, B\}\| = 2)$
129	128 70	sylibr	$⊢ (φ \land A \neq B) \to \{A, B\} \in P$
130		raleq	$⊢ p = \{A, B\} \to (\forall x \in p (x = A \lor x = B) \leftrightarrow \forall x \in \{A, B\} (x = A \lor x = B))$
131		eqeq1	$⊢ p = \{A, B\} \to (p = y \leftrightarrow \{A, B\} = y)$
132	131	imbi2d	$⊢ p = \{A, B\} \to ((\forall x \in y (x = A \lor x = B) \to p = y) \leftrightarrow (\forall x \in y (x = A \lor x = B) \to \{A, B\} = y))$
133	132	ralbidv	$⊢ p = \{A, B\} \to (\forall y \in P (\forall x \in y (x = A \lor x = B) \to p = y) \leftrightarrow \forall y \in P (\forall x \in y (x = A \lor x = B) \to \{A, B\} = y))$
134	130 133	anbi12d	$⊢ p = \{A, B\} \to ((\forall x \in p (x = A \lor x = B) \land \forall y \in P (\forall x \in y (x = A \lor x = B) \to p = y)) \leftrightarrow (\forall x \in \{A, B\} (x = A \lor x = B) \land \forall y \in P (\forall x \in y (x = A \lor x = B) \to \{A, B\} = y)))$
135	134	adantl	$⊢ ((φ \land A \neq B) \land p = \{A, B\}) \to ((\forall x \in p (x = A \lor x = B) \land \forall y \in P (\forall x \in y (x = A \lor x = B) \to p = y)) \leftrightarrow (\forall x \in \{A, B\} (x = A \lor x = B) \land \forall y \in P (\forall x \in y (x = A \lor x = B) \to \{A, B\} = y)))$
136		vex	$⊢ x \in V$
137	136	elpr	$⊢ x \in \{A, B\} \leftrightarrow (x = A \lor x = B)$
138	137	a1i	$⊢ (φ \land A \neq B) \to (x \in \{A, B\} \leftrightarrow (x = A \lor x = B))$
139	138	biimpd	$⊢ (φ \land A \neq B) \to (x \in \{A, B\} \to (x = A \lor x = B))$
140	139	imp	$⊢ ((φ \land A \neq B) \land x \in \{A, B\}) \to (x = A \lor x = B)$
141	140	ralrimiva	$⊢ (φ \land A \neq B) \to \forall x \in \{A, B\} (x = A \lor x = B)$
142	3	eleq2i	$⊢ y \in P \leftrightarrow y \in \{x \in 𝒫 V \| \|x\| = 2\}$
143		elss2prb	$⊢ y \in \{x \in 𝒫 V \| \|x\| = 2\} \leftrightarrow \exists a \in V \exists b \in V (a \neq b \land y = \{a, b\})$
144	142 143	bitri	$⊢ y \in P \leftrightarrow \exists a \in V \exists b \in V (a \neq b \land y = \{a, b\})$
145		prid1g	$⊢ a \in V \to a \in \{a, b\}$
146	145	ad2antrl	$⊢ ((φ \land A \neq B) \land (a \in V \land b \in V)) \to a \in \{a, b\}$
147	146	adantr	$⊢ (((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to a \in \{a, b\}$
148		eleq2	$⊢ y = \{a, b\} \to (a \in y \leftrightarrow a \in \{a, b\})$
149	148	ad2antll	$⊢ (((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to (a \in y \leftrightarrow a \in \{a, b\})$
150	147 149	mpbird	$⊢ (((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to a \in y$
151	14	rspcv	$⊢ a \in y \to (\forall x \in y (x = A \lor x = B) \to (a = A \lor a = B))$
152	150 151	syl	$⊢ (((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to (\forall x \in y (x = A \lor x = B) \to (a = A \lor a = B))$
153		prid2g	$⊢ b \in V \to b \in \{a, b\}$
154	153	ad2antll	$⊢ ((φ \land A \neq B) \land (a \in V \land b \in V)) \to b \in \{a, b\}$
155	154	adantr	$⊢ (((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to b \in \{a, b\}$
156		eleq2	$⊢ y = \{a, b\} \to (b \in y \leftrightarrow b \in \{a, b\})$
157	156	ad2antll	$⊢ (((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to (b \in y \leftrightarrow b \in \{a, b\})$
158	155 157	mpbird	$⊢ (((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to b \in y$
159	17	rspcv	$⊢ b \in y \to (\forall x \in y (x = A \lor x = B) \to (b = A \lor b = B))$
160	158 159	syl	$⊢ (((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to (\forall x \in y (x = A \lor x = B) \to (b = A \lor b = B))$
161		simplrr	$⊢ ((((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \land ((b = A \lor b = B) \land (a = A \lor a = B))) \to y = \{a, b\}$
162		eqtr3	$⊢ (a = A \land b = A) \to a = b$
163		eqneqall	$⊢ a = b \to (a \neq b \to \{a, b\} = \{A, B\})$
164	163	com12	$⊢ a \neq b \to (a = b \to \{a, b\} = \{A, B\})$
165	164	ad2antrl	$⊢ (((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to (a = b \to \{a, b\} = \{A, B\})$
166	165	com12	$⊢ a = b \to ((((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to \{a, b\} = \{A, B\})$
167	162 166	syl	$⊢ (a = A \land b = A) \to ((((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to \{a, b\} = \{A, B\})$
168	167	ex	$⊢ a = A \to (b = A \to ((((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to \{a, b\} = \{A, B\}))$
169	52	a1d	$⊢ (b = A \land a = B) \to ((((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to \{a, b\} = \{A, B\})$
170	169	expcom	$⊢ a = B \to (b = A \to ((((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to \{a, b\} = \{A, B\}))$
171	168 170	jaoi	$⊢ (a = A \lor a = B) \to (b = A \to ((((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to \{a, b\} = \{A, B\}))$
172	171	com12	$⊢ b = A \to ((a = A \lor a = B) \to ((((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to \{a, b\} = \{A, B\}))$
173	44	a1d	$⊢ (a = A \land b = B) \to ((((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to \{a, b\} = \{A, B\})$
174	173	ex	$⊢ a = A \to (b = B \to ((((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to \{a, b\} = \{A, B\}))$
175		eqtr3	$⊢ (a = B \land b = B) \to a = b$
176	175 166	syl	$⊢ (a = B \land b = B) \to ((((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to \{a, b\} = \{A, B\})$
177	176	ex	$⊢ a = B \to (b = B \to ((((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to \{a, b\} = \{A, B\}))$
178	174 177	jaoi	$⊢ (a = A \lor a = B) \to (b = B \to ((((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to \{a, b\} = \{A, B\}))$
179	178	com12	$⊢ b = B \to ((a = A \lor a = B) \to ((((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to \{a, b\} = \{A, B\}))$
180	172 179	jaoi	$⊢ (b = A \lor b = B) \to ((a = A \lor a = B) \to ((((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to \{a, b\} = \{A, B\}))$
181	180	imp	$⊢ ((b = A \lor b = B) \land (a = A \lor a = B)) \to ((((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to \{a, b\} = \{A, B\})$
182	181	impcom	$⊢ ((((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \land ((b = A \lor b = B) \land (a = A \lor a = B))) \to \{a, b\} = \{A, B\}$
183	161 182	eqtr2d	$⊢ ((((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \land ((b = A \lor b = B) \land (a = A \lor a = B))) \to \{A, B\} = y$
184	183	exp32	$⊢ (((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to ((b = A \lor b = B) \to ((a = A \lor a = B) \to \{A, B\} = y))$
185	160 184	syld	$⊢ (((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to (\forall x \in y (x = A \lor x = B) \to ((a = A \lor a = B) \to \{A, B\} = y))$
186	152 185	mpdd	$⊢ (((φ \land A \neq B) \land (a \in V \land b \in V)) \land (a \neq b \land y = \{a, b\})) \to (\forall x \in y (x = A \lor x = B) \to \{A, B\} = y)$
187	186	ex	$⊢ ((φ \land A \neq B) \land (a \in V \land b \in V)) \to ((a \neq b \land y = \{a, b\}) \to (\forall x \in y (x = A \lor x = B) \to \{A, B\} = y))$
188	187	rexlimdvva	$⊢ (φ \land A \neq B) \to (\exists a \in V \exists b \in V (a \neq b \land y = \{a, b\}) \to (\forall x \in y (x = A \lor x = B) \to \{A, B\} = y))$
189	144 188	syl5bi	$⊢ (φ \land A \neq B) \to (y \in P \to (\forall x \in y (x = A \lor x = B) \to \{A, B\} = y))$
190	189	imp	$⊢ ((φ \land A \neq B) \land y \in P) \to (\forall x \in y (x = A \lor x = B) \to \{A, B\} = y)$
191	190	ralrimiva	$⊢ (φ \land A \neq B) \to \forall y \in P (\forall x \in y (x = A \lor x = B) \to \{A, B\} = y)$
192	141 191	jca	$⊢ (φ \land A \neq B) \to (\forall x \in \{A, B\} (x = A \lor x = B) \land \forall y \in P (\forall x \in y (x = A \lor x = B) \to \{A, B\} = y))$
193	129 135 192	rspcedvd	$⊢ (φ \land A \neq B) \to \exists p \in P (\forall x \in p (x = A \lor x = B) \land \forall y \in P (\forall x \in y (x = A \lor x = B) \to p = y))$
194		raleq	$⊢ p = y \to (\forall x \in p (x = A \lor x = B) \leftrightarrow \forall x \in y (x = A \lor x = B))$
195	194	reu8	$⊢ \exists! p \in P \forall x \in p (x = A \lor x = B) \leftrightarrow \exists p \in P (\forall x \in p (x = A \lor x = B) \land \forall y \in P (\forall x \in y (x = A \lor x = B) \to p = y))$
196	193 195	sylibr	$⊢ (φ \land A \neq B) \to \exists! p \in P \forall x \in p (x = A \lor x = B)$
197	196	ex	$⊢ φ \to (A \neq B \to \exists! p \in P \forall x \in p (x = A \lor x = B))$
198	122 197	impbid	$⊢ φ \to (\exists! p \in P \forall x \in p (x = A \lor x = B) \leftrightarrow A \neq B)$

Metamath Proof Explorer

Theorem paireqne

Proof