Theorem ichnreuop

Description: If the setvar variables are interchangeable in a wff, there is never a unique ordered pair with different components fulfilling the wff (because if <. a , b >. fulfils the wff, then also <. b , a >. fulfils the wff). (Contributed by AV, 27-Aug-2023)

	Ref	Expression
Assertion	ichnreuop	$$⊢\left[a\rightleftarrows b\right]\phi \to \neg \exists !p\in \left(X\times X\right)\exists a\exists b\left(p=⟨a,b⟩\wedge a\ne b\wedge \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		notnotb	$$⊢\exists a\exists b\left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\leftrightarrow \neg \neg \exists a\exists b\left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)$$
2		nfv	$$⊢Ⅎc\left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)$$
3		nfv	$$⊢Ⅎd\left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)$$
4		nfv	$$⊢Ⅎa⟨x,y⟩=⟨c,d⟩$$
5		nfv	$$⊢Ⅎac\ne d$$
6		nfsbc1v	$$⊢Ⅎa\underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi$$
7	4 5 6	nf3an	$$⊢Ⅎa\left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)$$
8		nfv	$$⊢Ⅎb⟨x,y⟩=⟨c,d⟩$$
9		nfv	$$⊢Ⅎbc\ne d$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}bc$$
11		nfsbc1v	$$⊢Ⅎb\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi$$
12	10 11	nfsbcw	$$⊢Ⅎb\underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi$$
13	8 9 12	nf3an	$$⊢Ⅎb\left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)$$
14		opeq12	$$⊢\left(a=c\wedge b=d\right)\to ⟨a,b⟩=⟨c,d⟩$$
15	14	eqeq2d	$$⊢\left(a=c\wedge b=d\right)\to \left(⟨x,y⟩=⟨a,b⟩\leftrightarrow ⟨x,y⟩=⟨c,d⟩\right)$$
16		simpl	$$⊢\left(a=c\wedge b=d\right)\to a=c$$
17		simpr	$$⊢\left(a=c\wedge b=d\right)\to b=d$$
18	16 17	neeq12d	$$⊢\left(a=c\wedge b=d\right)\to \left(a\ne b\leftrightarrow c\ne d\right)$$
19		sbceq1a	$$⊢b=d\to \left(\phi \leftrightarrow \underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)$$
20		sbceq1a	$$⊢a=c\to \left(\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)$$
21	19 20	sylan9bbr	$$⊢\left(a=c\wedge b=d\right)\to \left(\phi \leftrightarrow \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)$$
22	15 18 21	3anbi123d	$$⊢\left(a=c\wedge b=d\right)\to \left(\left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\leftrightarrow \left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\right)$$
23	2 3 7 13 22	cbvex2v	$$⊢\exists a\exists b\left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\leftrightarrow \exists c\exists d\left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)$$
24		vex	$$⊢x\in \mathrm{V}$$
25		vex	$$⊢y\in \mathrm{V}$$
26	24 25	opth	$$⊢⟨x,y⟩=⟨c,d⟩\leftrightarrow \left(x=c\wedge y=d\right)$$
27		eleq1w	$$⊢y=d\to \left(y\in X\leftrightarrow d\in X\right)$$
28	27	biimpcd	$$⊢y\in X\to \left(y=d\to d\in X\right)$$
29	28	adantl	$$⊢\left(x\in X\wedge y\in X\right)\to \left(y=d\to d\in X\right)$$
30	29	adantl	$$⊢\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to \left(y=d\to d\in X\right)$$
31	30	com12	$$⊢y=d\to \left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to d\in X\right)$$
32	31	adantl	$$⊢\left(x=c\wedge y=d\right)\to \left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to d\in X\right)$$
33	26 32	sylbi	$$⊢⟨x,y⟩=⟨c,d⟩\to \left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to d\in X\right)$$
34	33	3ad2ant1	$$⊢\left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\to \left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to d\in X\right)$$
35	34	impcom	$$⊢\left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\wedge \left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\right)\to d\in X$$
36		eleq1w	$$⊢x=c\to \left(x\in X\leftrightarrow c\in X\right)$$
37	36	biimpcd	$$⊢x\in X\to \left(x=c\to c\in X\right)$$
38	37	adantr	$$⊢\left(x\in X\wedge y\in X\right)\to \left(x=c\to c\in X\right)$$
39	38	adantl	$$⊢\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to \left(x=c\to c\in X\right)$$
40	39	com12	$$⊢x=c\to \left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to c\in X\right)$$
41	40	adantr	$$⊢\left(x=c\wedge y=d\right)\to \left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to c\in X\right)$$
42	26 41	sylbi	$$⊢⟨x,y⟩=⟨c,d⟩\to \left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to c\in X\right)$$
43	42	3ad2ant1	$$⊢\left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\to \left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to c\in X\right)$$
44	43	impcom	$$⊢\left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\wedge \left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\right)\to c\in X$$
45		eqidd	$$⊢\left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\wedge \left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\right)\to ⟨d,c⟩=⟨d,c⟩$$
46		necom	$$⊢c\ne d\leftrightarrow d\ne c$$
47	46	biimpi	$$⊢c\ne d\to d\ne c$$
48	47	3ad2ant2	$$⊢\left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\to d\ne c$$
49	48	adantl	$$⊢\left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\wedge \left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\right)\to d\ne c$$
50		dfich2	$$⊢\left[a\rightleftarrows b\right]\phi \leftrightarrow \forall c\forall d\left(\left[c/a\right]\left[d/b\right]\phi \leftrightarrow \left[d/a\right]\left[c/b\right]\phi \right)$$
51		2sp	$$⊢\forall c\forall d\left(\left[c/a\right]\left[d/b\right]\phi \leftrightarrow \left[d/a\right]\left[c/b\right]\phi \right)\to \left(\left[c/a\right]\left[d/b\right]\phi \leftrightarrow \left[d/a\right]\left[c/b\right]\phi \right)$$
52		sbsbc	$$⊢\left[d/b\right]\phi \leftrightarrow \underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi$$
53	52	sbbii	$$⊢\left[c/a\right]\left[d/b\right]\phi \leftrightarrow \left[c/a\right]\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi$$
54		sbsbc	$$⊢\left[c/a\right]\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi$$
55	53 54	bitri	$$⊢\left[c/a\right]\left[d/b\right]\phi \leftrightarrow \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi$$
56		sbsbc	$$⊢\left[c/b\right]\phi \leftrightarrow \underset{\dot{}}{[}c/b\underset{\dot{}}{]}\phi$$
57	56	sbbii	$$⊢\left[d/a\right]\left[c/b\right]\phi \leftrightarrow \left[d/a\right]\underset{\dot{}}{[}c/b\underset{\dot{}}{]}\phi$$
58		sbsbc	$$⊢\left[d/a\right]\underset{\dot{}}{[}c/b\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\underset{\dot{}}{[}c/b\underset{\dot{}}{]}\phi$$
59	57 58	bitri	$$⊢\left[d/a\right]\left[c/b\right]\phi \leftrightarrow \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\underset{\dot{}}{[}c/b\underset{\dot{}}{]}\phi$$
60	51 55 59	3bitr3g	$$⊢\forall c\forall d\left(\left[c/a\right]\left[d/b\right]\phi \leftrightarrow \left[d/a\right]\left[c/b\right]\phi \right)\to \left(\underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\underset{\dot{}}{[}c/b\underset{\dot{}}{]}\phi \right)$$
61	60	biimpd	$$⊢\forall c\forall d\left(\left[c/a\right]\left[d/b\right]\phi \leftrightarrow \left[d/a\right]\left[c/b\right]\phi \right)\to \left(\underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\underset{\dot{}}{[}c/b\underset{\dot{}}{]}\phi \right)$$
62	50 61	sylbi	$$⊢\left[a\rightleftarrows b\right]\phi \to \left(\underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\underset{\dot{}}{[}c/b\underset{\dot{}}{]}\phi \right)$$
63	62	adantr	$$⊢\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to \left(\underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\underset{\dot{}}{[}c/b\underset{\dot{}}{]}\phi \right)$$
64	63	com12	$$⊢\underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \to \left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\underset{\dot{}}{[}c/b\underset{\dot{}}{]}\phi \right)$$
65	64	3ad2ant3	$$⊢\left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\to \left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\underset{\dot{}}{[}c/b\underset{\dot{}}{]}\phi \right)$$
66	65	impcom	$$⊢\left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\wedge \left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\right)\to \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\underset{\dot{}}{[}c/b\underset{\dot{}}{]}\phi$$
67		sbccom	$$⊢\underset{\dot{}}{[}c/b\underset{\dot{}}{]}\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\underset{\dot{}}{[}c/b\underset{\dot{}}{]}\phi$$
68	66 67	sylibr	$$⊢\left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\wedge \left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\right)\to \underset{\dot{}}{[}c/b\underset{\dot{}}{]}\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi$$
69	45 49 68	3jca	$$⊢\left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\wedge \left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\right)\to \left(⟨d,c⟩=⟨d,c⟩\wedge d\ne c\wedge \underset{\dot{}}{[}c/b\underset{\dot{}}{]}\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)$$
70		nfv	$$⊢Ⅎb⟨d,c⟩=⟨d,c⟩$$
71		nfv	$$⊢Ⅎbd\ne c$$
72		nfsbc1v	$$⊢Ⅎb\underset{\dot{}}{[}c/b\underset{\dot{}}{]}\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi$$
73	70 71 72	nf3an	$$⊢Ⅎb\left(⟨d,c⟩=⟨d,c⟩\wedge d\ne c\wedge \underset{\dot{}}{[}c/b\underset{\dot{}}{]}\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)$$
74		opeq2	$$⊢b=c\to ⟨d,b⟩=⟨d,c⟩$$
75	74	eqeq2d	$$⊢b=c\to \left(⟨d,c⟩=⟨d,b⟩\leftrightarrow ⟨d,c⟩=⟨d,c⟩\right)$$
76		neeq2	$$⊢b=c\to \left(d\ne b\leftrightarrow d\ne c\right)$$
77		sbceq1a	$$⊢b=c\to \left(\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}c/b\underset{\dot{}}{]}\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)$$
78	75 76 77	3anbi123d	$$⊢b=c\to \left(\left(⟨d,c⟩=⟨d,b⟩\wedge d\ne b\wedge \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(⟨d,c⟩=⟨d,c⟩\wedge d\ne c\wedge \underset{\dot{}}{[}c/b\underset{\dot{}}{]}\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)\right)$$
79	10 73 78	spcegf	$$⊢c\in X\to \left(\left(⟨d,c⟩=⟨d,c⟩\wedge d\ne c\wedge \underset{\dot{}}{[}c/b\underset{\dot{}}{]}\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)\to \exists b\left(⟨d,c⟩=⟨d,b⟩\wedge d\ne b\wedge \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)\right)$$
80	44 69 79	sylc	$$⊢\left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\wedge \left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\right)\to \exists b\left(⟨d,c⟩=⟨d,b⟩\wedge d\ne b\wedge \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)$$
81		nfcv	$$⊢\underset{\_}{Ⅎ}ad$$
82		nfv	$$⊢Ⅎa⟨d,c⟩=⟨d,b⟩$$
83		nfv	$$⊢Ⅎad\ne b$$
84		nfsbc1v	$$⊢Ⅎa\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi$$
85	82 83 84	nf3an	$$⊢Ⅎa\left(⟨d,c⟩=⟨d,b⟩\wedge d\ne b\wedge \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)$$
86	85	nfex	$$⊢Ⅎa\exists b\left(⟨d,c⟩=⟨d,b⟩\wedge d\ne b\wedge \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)$$
87		opeq1	$$⊢a=d\to ⟨a,b⟩=⟨d,b⟩$$
88	87	eqeq2d	$$⊢a=d\to \left(⟨d,c⟩=⟨a,b⟩\leftrightarrow ⟨d,c⟩=⟨d,b⟩\right)$$
89		neeq1	$$⊢a=d\to \left(a\ne b\leftrightarrow d\ne b\right)$$
90		sbceq1a	$$⊢a=d\to \left(\phi \leftrightarrow \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)$$
91	88 89 90	3anbi123d	$$⊢a=d\to \left(\left(⟨d,c⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\leftrightarrow \left(⟨d,c⟩=⟨d,b⟩\wedge d\ne b\wedge \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)\right)$$
92	91	exbidv	$$⊢a=d\to \left(\exists b\left(⟨d,c⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\leftrightarrow \exists b\left(⟨d,c⟩=⟨d,b⟩\wedge d\ne b\wedge \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)\right)$$
93	81 86 92	spcegf	$$⊢d\in X\to \left(\exists b\left(⟨d,c⟩=⟨d,b⟩\wedge d\ne b\wedge \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)\to \exists a\exists b\left(⟨d,c⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\right)$$
94	35 80 93	sylc	$$⊢\left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\wedge \left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\right)\to \exists a\exists b\left(⟨d,c⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)$$
95		vex	$$⊢d\in \mathrm{V}$$
96		vex	$$⊢c\in \mathrm{V}$$
97	95 96	opth1	$$⊢⟨d,c⟩=⟨c,d⟩\to d=c$$
98	97	equcomd	$$⊢⟨d,c⟩=⟨c,d⟩\to c=d$$
99	98	necon3ai	$$⊢c\ne d\to \neg ⟨d,c⟩=⟨c,d⟩$$
100	99	adantl	$$⊢\left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\right)\to \neg ⟨d,c⟩=⟨c,d⟩$$
101		eqeq2	$$⊢⟨x,y⟩=⟨c,d⟩\to \left(⟨d,c⟩=⟨x,y⟩\leftrightarrow ⟨d,c⟩=⟨c,d⟩\right)$$
102	101	adantr	$$⊢\left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\right)\to \left(⟨d,c⟩=⟨x,y⟩\leftrightarrow ⟨d,c⟩=⟨c,d⟩\right)$$
103	100 102	mtbird	$$⊢\left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\right)\to \neg ⟨d,c⟩=⟨x,y⟩$$
104	103	3adant3	$$⊢\left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\to \neg ⟨d,c⟩=⟨x,y⟩$$
105	104	adantl	$$⊢\left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\wedge \left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\right)\to \neg ⟨d,c⟩=⟨x,y⟩$$
106	94 105	jcnd	$$⊢\left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\wedge \left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\right)\to \neg \left(\exists a\exists b\left(⟨d,c⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨d,c⟩=⟨x,y⟩\right)$$
107		opeq1	$$⊢v=d\to ⟨v,w⟩=⟨d,w⟩$$
108	107	eqeq1d	$$⊢v=d\to \left(⟨v,w⟩=⟨a,b⟩\leftrightarrow ⟨d,w⟩=⟨a,b⟩\right)$$
109	108	3anbi1d	$$⊢v=d\to \left(\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\leftrightarrow \left(⟨d,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\right)$$
110	109	2exbidv	$$⊢v=d\to \left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\leftrightarrow \exists a\exists b\left(⟨d,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\right)$$
111	107	eqeq1d	$$⊢v=d\to \left(⟨v,w⟩=⟨x,y⟩\leftrightarrow ⟨d,w⟩=⟨x,y⟩\right)$$
112	110 111	imbi12d	$$⊢v=d\to \left(\left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)\leftrightarrow \left(\exists a\exists b\left(⟨d,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨d,w⟩=⟨x,y⟩\right)\right)$$
113	112	notbid	$$⊢v=d\to \left(\neg \left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)\leftrightarrow \neg \left(\exists a\exists b\left(⟨d,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨d,w⟩=⟨x,y⟩\right)\right)$$
114		opeq2	$$⊢w=c\to ⟨d,w⟩=⟨d,c⟩$$
115	114	eqeq1d	$$⊢w=c\to \left(⟨d,w⟩=⟨a,b⟩\leftrightarrow ⟨d,c⟩=⟨a,b⟩\right)$$
116	115	3anbi1d	$$⊢w=c\to \left(\left(⟨d,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\leftrightarrow \left(⟨d,c⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\right)$$
117	116	2exbidv	$$⊢w=c\to \left(\exists a\exists b\left(⟨d,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\leftrightarrow \exists a\exists b\left(⟨d,c⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\right)$$
118	114	eqeq1d	$$⊢w=c\to \left(⟨d,w⟩=⟨x,y⟩\leftrightarrow ⟨d,c⟩=⟨x,y⟩\right)$$
119	117 118	imbi12d	$$⊢w=c\to \left(\left(\exists a\exists b\left(⟨d,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨d,w⟩=⟨x,y⟩\right)\leftrightarrow \left(\exists a\exists b\left(⟨d,c⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨d,c⟩=⟨x,y⟩\right)\right)$$
120	119	notbid	$$⊢w=c\to \left(\neg \left(\exists a\exists b\left(⟨d,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨d,w⟩=⟨x,y⟩\right)\leftrightarrow \neg \left(\exists a\exists b\left(⟨d,c⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨d,c⟩=⟨x,y⟩\right)\right)$$
121	113 120	rspc2ev	$$⊢\left(d\in X\wedge c\in X\wedge \neg \left(\exists a\exists b\left(⟨d,c⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨d,c⟩=⟨x,y⟩\right)\right)\to \exists v\in X\exists w\in X\neg \left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)$$
122	35 44 106 121	syl3anc	$$⊢\left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\wedge \left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\right)\to \exists v\in X\exists w\in X\neg \left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)$$
123		rexnal2	$$⊢\exists v\in X\exists w\in X\neg \left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)\leftrightarrow \neg \forall v\in X\forall w\in X\left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)$$
124	122 123	sylib	$$⊢\left(\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\wedge \left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\right)\to \neg \forall v\in X\forall w\in X\left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)$$
125	124	ex	$$⊢\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to \left(\left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\to \neg \forall v\in X\forall w\in X\left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)\right)$$
126	125	exlimdvv	$$⊢\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to \left(\exists c\exists d\left(⟨x,y⟩=⟨c,d⟩\wedge c\ne d\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\underset{\dot{}}{[}d/b\underset{\dot{}}{]}\phi \right)\to \neg \forall v\in X\forall w\in X\left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)\right)$$
127	23 126	syl5bi	$$⊢\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to \left(\exists a\exists b\left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to \neg \forall v\in X\forall w\in X\left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)\right)$$
128	1 127	syl5bir	$$⊢\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to \left(\neg \neg \exists a\exists b\left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to \neg \forall v\in X\forall w\in X\left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)\right)$$
129	128	orrd	$$⊢\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to \left(\neg \exists a\exists b\left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\vee \neg \forall v\in X\forall w\in X\left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)\right)$$
130		ianor	$$⊢\neg \left(\exists a\exists b\left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\wedge \forall v\in X\forall w\in X\left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)\right)\leftrightarrow \left(\neg \exists a\exists b\left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\vee \neg \forall v\in X\forall w\in X\left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)\right)$$
131	129 130	sylibr	$$⊢\left(\left[a\rightleftarrows b\right]\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to \neg \left(\exists a\exists b\left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\wedge \forall v\in X\forall w\in X\left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)\right)$$
132	131	ralrimivva	$$⊢\left[a\rightleftarrows b\right]\phi \to \forall x\in X\forall y\in X\neg \left(\exists a\exists b\left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\wedge \forall v\in X\forall w\in X\left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)\right)$$
133		ralnex2	$$⊢\forall x\in X\forall y\in X\neg \left(\exists a\exists b\left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\wedge \forall v\in X\forall w\in X\left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)\right)\leftrightarrow \neg \exists x\in X\exists y\in X\left(\exists a\exists b\left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\wedge \forall v\in X\forall w\in X\left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)\right)$$
134	132 133	sylib	$$⊢\left[a\rightleftarrows b\right]\phi \to \neg \exists x\in X\exists y\in X\left(\exists a\exists b\left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\wedge \forall v\in X\forall w\in X\left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)\right)$$
135		eqeq1	$$⊢p=⟨x,y⟩\to \left(p=⟨a,b⟩\leftrightarrow ⟨x,y⟩=⟨a,b⟩\right)$$
136	135	3anbi1d	$$⊢p=⟨x,y⟩\to \left(\left(p=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\leftrightarrow \left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\right)$$
137	136	2exbidv	$$⊢p=⟨x,y⟩\to \left(\exists a\exists b\left(p=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\leftrightarrow \exists a\exists b\left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\right)$$
138		eqeq1	$$⊢p=⟨v,w⟩\to \left(p=⟨a,b⟩\leftrightarrow ⟨v,w⟩=⟨a,b⟩\right)$$
139	138	3anbi1d	$$⊢p=⟨v,w⟩\to \left(\left(p=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\leftrightarrow \left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\right)$$
140	139	2exbidv	$$⊢p=⟨v,w⟩\to \left(\exists a\exists b\left(p=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\leftrightarrow \exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\right)$$
141	137 140	reuop	$$⊢\exists !p\in \left(X\times X\right)\exists a\exists b\left(p=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\leftrightarrow \exists x\in X\exists y\in X\left(\exists a\exists b\left(⟨x,y⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\wedge \forall v\in X\forall w\in X\left(\exists a\exists b\left(⟨v,w⟩=⟨a,b⟩\wedge a\ne b\wedge \phi \right)\to ⟨v,w⟩=⟨x,y⟩\right)\right)$$
142	134 141	sylnibr	$$⊢\left[a\rightleftarrows b\right]\phi \to \neg \exists !p\in \left(X\times X\right)\exists a\exists b\left(p=⟨a,b⟩\wedge a\ne b\wedge \phi \right)$$