ichreuopeq

Description: If the setvar variables are interchangeable in a wff, and there is a unique ordered pair fulfilling the wff, then both setvar variables must be equal. (Contributed by AV, 28-Aug-2023)

		Ref	Expression
	Assertion	ichreuopeq	$⊢ [a ⇄ b] φ \to (\exists! p \in (X \times X) \exists a \exists b (p = ⟨a, b⟩ \land φ) \to \exists a \exists b (a = b \land φ))$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$⊢ p = ⟨x, y⟩ \to (p = ⟨a, b⟩ \leftrightarrow ⟨x, y⟩ = ⟨a, b⟩)$
2	1	anbi1d	$⊢ p = ⟨x, y⟩ \to ((p = ⟨a, b⟩ \land φ) \leftrightarrow (⟨x, y⟩ = ⟨a, b⟩ \land φ))$
3	2	2exbidv	$⊢ p = ⟨x, y⟩ \to (\exists a \exists b (p = ⟨a, b⟩ \land φ) \leftrightarrow \exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ))$
4		eqeq1	$⊢ p = ⟨v, w⟩ \to (p = ⟨a, b⟩ \leftrightarrow ⟨v, w⟩ = ⟨a, b⟩)$
5	4	anbi1d	$⊢ p = ⟨v, w⟩ \to ((p = ⟨a, b⟩ \land φ) \leftrightarrow (⟨v, w⟩ = ⟨a, b⟩ \land φ))$
6	5	2exbidv	$⊢ p = ⟨v, w⟩ \to (\exists a \exists b (p = ⟨a, b⟩ \land φ) \leftrightarrow \exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ))$
7	3 6	reuop	$⊢ \exists! p \in (X \times X) \exists a \exists b (p = ⟨a, b⟩ \land φ) \leftrightarrow \exists x \in X \exists y \in X (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall v \in X \forall w \in X (\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \to ⟨v, w⟩ = ⟨x, y⟩))$
8		nfich1	$⊢ Ⅎ a [a ⇄ b] φ$
9		nfv	$⊢ Ⅎ a (x \in X \land y \in X)$
10	8 9	nfan	$⊢ Ⅎ a ([a ⇄ b] φ \land (x \in X \land y \in X))$
11		nfcv	$⊢ \underline{Ⅎ} a X$
12		nfe1	$⊢ Ⅎ a \exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ)$
13		nfv	$⊢ Ⅎ a ⟨v, w⟩ = ⟨x, y⟩$
14	12 13	nfim	$⊢ Ⅎ a (\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \to ⟨v, w⟩ = ⟨x, y⟩)$
15	11 14	nfralw	$⊢ Ⅎ a \forall w \in X (\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \to ⟨v, w⟩ = ⟨x, y⟩)$
16	11 15	nfralw	$⊢ Ⅎ a \forall v \in X \forall w \in X (\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \to ⟨v, w⟩ = ⟨x, y⟩)$
17		nfe1	$⊢ Ⅎ a \exists a \exists b (a = b \land φ)$
18	16 17	nfim	$⊢ Ⅎ a (\forall v \in X \forall w \in X (\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \to ⟨v, w⟩ = ⟨x, y⟩) \to \exists a \exists b (a = b \land φ))$
19		nfich2	$⊢ Ⅎ b [a ⇄ b] φ$
20		nfv	$⊢ Ⅎ b (x \in X \land y \in X)$
21	19 20	nfan	$⊢ Ⅎ b ([a ⇄ b] φ \land (x \in X \land y \in X))$
22		nfcv	$⊢ \underline{Ⅎ} b X$
23		nfe1	$⊢ Ⅎ b \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ)$
24	23	nfex	$⊢ Ⅎ b \exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ)$
25		nfv	$⊢ Ⅎ b ⟨v, w⟩ = ⟨x, y⟩$
26	24 25	nfim	$⊢ Ⅎ b (\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \to ⟨v, w⟩ = ⟨x, y⟩)$
27	22 26	nfralw	$⊢ Ⅎ b \forall w \in X (\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \to ⟨v, w⟩ = ⟨x, y⟩)$
28	22 27	nfralw	$⊢ Ⅎ b \forall v \in X \forall w \in X (\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \to ⟨v, w⟩ = ⟨x, y⟩)$
29		nfe1	$⊢ Ⅎ b \exists b (a = b \land φ)$
30	29	nfex	$⊢ Ⅎ b \exists a \exists b (a = b \land φ)$
31	28 30	nfim	$⊢ Ⅎ b (\forall v \in X \forall w \in X (\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \to ⟨v, w⟩ = ⟨x, y⟩) \to \exists a \exists b (a = b \land φ))$
32		opeq12	$⊢ (v = y \land w = x) \to ⟨v, w⟩ = ⟨y, x⟩$
33	32	eqeq1d	$⊢ (v = y \land w = x) \to (⟨v, w⟩ = ⟨a, b⟩ \leftrightarrow ⟨y, x⟩ = ⟨a, b⟩)$
34	33	anbi1d	$⊢ (v = y \land w = x) \to ((⟨v, w⟩ = ⟨a, b⟩ \land φ) \leftrightarrow (⟨y, x⟩ = ⟨a, b⟩ \land φ))$
35	34	2exbidv	$⊢ (v = y \land w = x) \to (\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \leftrightarrow \exists a \exists b (⟨y, x⟩ = ⟨a, b⟩ \land φ))$
36	32	eqeq1d	$⊢ (v = y \land w = x) \to (⟨v, w⟩ = ⟨x, y⟩ \leftrightarrow ⟨y, x⟩ = ⟨x, y⟩)$
37	35 36	imbi12d	$⊢ (v = y \land w = x) \to ((\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \to ⟨v, w⟩ = ⟨x, y⟩) \leftrightarrow (\exists a \exists b (⟨y, x⟩ = ⟨a, b⟩ \land φ) \to ⟨y, x⟩ = ⟨x, y⟩))$
38	37	rspc2gv	$⊢ (y \in X \land x \in X) \to (\forall v \in X \forall w \in X (\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \to ⟨v, w⟩ = ⟨x, y⟩) \to (\exists a \exists b (⟨y, x⟩ = ⟨a, b⟩ \land φ) \to ⟨y, x⟩ = ⟨x, y⟩))$
39	38	ancoms	$⊢ (x \in X \land y \in X) \to (\forall v \in X \forall w \in X (\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \to ⟨v, w⟩ = ⟨x, y⟩) \to (\exists a \exists b (⟨y, x⟩ = ⟨a, b⟩ \land φ) \to ⟨y, x⟩ = ⟨x, y⟩))$
40	39	adantl	$⊢ ([a ⇄ b] φ \land (x \in X \land y \in X)) \to (\forall v \in X \forall w \in X (\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \to ⟨v, w⟩ = ⟨x, y⟩) \to (\exists a \exists b (⟨y, x⟩ = ⟨a, b⟩ \land φ) \to ⟨y, x⟩ = ⟨x, y⟩))$
41		simprr	$⊢ ([a ⇄ b] φ \land (x \in X \land y \in X)) \to y \in X$
42	41	adantr	$⊢ (([a ⇄ b] φ \land (x \in X \land y \in X)) \land (⟨x, y⟩ = ⟨a, b⟩ \land φ)) \to y \in X$
43		simpl	$⊢ (x \in X \land y \in X) \to x \in X$
44	43	adantl	$⊢ ([a ⇄ b] φ \land (x \in X \land y \in X)) \to x \in X$
45	44	adantr	$⊢ (([a ⇄ b] φ \land (x \in X \land y \in X)) \land (⟨x, y⟩ = ⟨a, b⟩ \land φ)) \to x \in X$
46		eqidd	$⊢ (([a ⇄ b] φ \land (x \in X \land y \in X)) \land (⟨x, y⟩ = ⟨a, b⟩ \land φ)) \to ⟨y, x⟩ = ⟨y, x⟩$
47		vex	$⊢ x \in V$
48		vex	$⊢ y \in V$
49	47 48	opth	$⊢ ⟨x, y⟩ = ⟨a, b⟩ \leftrightarrow (x = a \land y = b)$
50		sbceq1a	$⊢ b = y \to (φ \leftrightarrow \underset{˙}{[} y / b \underset{˙}{]} φ)$
51	50	equcoms	$⊢ y = b \to (φ \leftrightarrow \underset{˙}{[} y / b \underset{˙}{]} φ)$
52		sbceq1a	$⊢ a = x \to (\underset{˙}{[} y / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} x / a \underset{˙}{]} \underset{˙}{[} y / b \underset{˙}{]} φ)$
53	52	equcoms	$⊢ x = a \to (\underset{˙}{[} y / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} x / a \underset{˙}{]} \underset{˙}{[} y / b \underset{˙}{]} φ)$
54	51 53	sylan9bbr	$⊢ (x = a \land y = b) \to (φ \leftrightarrow \underset{˙}{[} x / a \underset{˙}{]} \underset{˙}{[} y / b \underset{˙}{]} φ)$
55		dfich2	$⊢ [a ⇄ b] φ \leftrightarrow \forall x \forall y ([x/ a] [y/ b] φ \leftrightarrow [y/ a] [x/ b] φ)$
56		2sp	$⊢ \forall x \forall y ([x/ a] [y/ b] φ \leftrightarrow [y/ a] [x/ b] φ) \to ([x/ a] [y/ b] φ \leftrightarrow [y/ a] [x/ b] φ)$
57		sbsbc	$⊢ [y/ b] φ \leftrightarrow \underset{˙}{[} y / b \underset{˙}{]} φ$
58	57	sbbii	$⊢ [x/ a] [y/ b] φ \leftrightarrow [x/ a] \underset{˙}{[} y / b \underset{˙}{]} φ$
59		sbsbc	$⊢ [x/ a] \underset{˙}{[} y / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} x / a \underset{˙}{]} \underset{˙}{[} y / b \underset{˙}{]} φ$
60	58 59	bitri	$⊢ [x/ a] [y/ b] φ \leftrightarrow \underset{˙}{[} x / a \underset{˙}{]} \underset{˙}{[} y / b \underset{˙}{]} φ$
61		sbsbc	$⊢ [x/ b] φ \leftrightarrow \underset{˙}{[} x / b \underset{˙}{]} φ$
62	61	sbbii	$⊢ [y/ a] [x/ b] φ \leftrightarrow [y/ a] \underset{˙}{[} x / b \underset{˙}{]} φ$
63		sbsbc	$⊢ [y/ a] \underset{˙}{[} x / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} y / a \underset{˙}{]} \underset{˙}{[} x / b \underset{˙}{]} φ$
64	62 63	bitri	$⊢ [y/ a] [x/ b] φ \leftrightarrow \underset{˙}{[} y / a \underset{˙}{]} \underset{˙}{[} x / b \underset{˙}{]} φ$
65	56 60 64	3bitr3g	$⊢ \forall x \forall y ([x/ a] [y/ b] φ \leftrightarrow [y/ a] [x/ b] φ) \to (\underset{˙}{[} x / a \underset{˙}{]} \underset{˙}{[} y / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} y / a \underset{˙}{]} \underset{˙}{[} x / b \underset{˙}{]} φ)$
66	55 65	sylbi	$⊢ [a ⇄ b] φ \to (\underset{˙}{[} x / a \underset{˙}{]} \underset{˙}{[} y / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} y / a \underset{˙}{]} \underset{˙}{[} x / b \underset{˙}{]} φ)$
67	66	biimpd	$⊢ [a ⇄ b] φ \to (\underset{˙}{[} x / a \underset{˙}{]} \underset{˙}{[} y / b \underset{˙}{]} φ \to \underset{˙}{[} y / a \underset{˙}{]} \underset{˙}{[} x / b \underset{˙}{]} φ)$
68	67	adantr	$⊢ ([a ⇄ b] φ \land (x \in X \land y \in X)) \to (\underset{˙}{[} x / a \underset{˙}{]} \underset{˙}{[} y / b \underset{˙}{]} φ \to \underset{˙}{[} y / a \underset{˙}{]} \underset{˙}{[} x / b \underset{˙}{]} φ)$
69	68	com12	$⊢ \underset{˙}{[} x / a \underset{˙}{]} \underset{˙}{[} y / b \underset{˙}{]} φ \to (([a ⇄ b] φ \land (x \in X \land y \in X)) \to \underset{˙}{[} y / a \underset{˙}{]} \underset{˙}{[} x / b \underset{˙}{]} φ)$
70	54 69	biimtrdi	$⊢ (x = a \land y = b) \to (φ \to (([a ⇄ b] φ \land (x \in X \land y \in X)) \to \underset{˙}{[} y / a \underset{˙}{]} \underset{˙}{[} x / b \underset{˙}{]} φ))$
71	49 70	sylbi	$⊢ ⟨x, y⟩ = ⟨a, b⟩ \to (φ \to (([a ⇄ b] φ \land (x \in X \land y \in X)) \to \underset{˙}{[} y / a \underset{˙}{]} \underset{˙}{[} x / b \underset{˙}{]} φ))$
72	71	imp	$⊢ (⟨x, y⟩ = ⟨a, b⟩ \land φ) \to (([a ⇄ b] φ \land (x \in X \land y \in X)) \to \underset{˙}{[} y / a \underset{˙}{]} \underset{˙}{[} x / b \underset{˙}{]} φ)$
73	72	impcom	$⊢ (([a ⇄ b] φ \land (x \in X \land y \in X)) \land (⟨x, y⟩ = ⟨a, b⟩ \land φ)) \to \underset{˙}{[} y / a \underset{˙}{]} \underset{˙}{[} x / b \underset{˙}{]} φ$
74		sbccom	$⊢ \underset{˙}{[} x / b \underset{˙}{]} \underset{˙}{[} y / a \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} y / a \underset{˙}{]} \underset{˙}{[} x / b \underset{˙}{]} φ$
75	73 74	sylibr	$⊢ (([a ⇄ b] φ \land (x \in X \land y \in X)) \land (⟨x, y⟩ = ⟨a, b⟩ \land φ)) \to \underset{˙}{[} x / b \underset{˙}{]} \underset{˙}{[} y / a \underset{˙}{]} φ$
76	46 75	jca	$⊢ (([a ⇄ b] φ \land (x \in X \land y \in X)) \land (⟨x, y⟩ = ⟨a, b⟩ \land φ)) \to (⟨y, x⟩ = ⟨y, x⟩ \land \underset{˙}{[} x / b \underset{˙}{]} \underset{˙}{[} y / a \underset{˙}{]} φ)$
77		nfcv	$⊢ \underline{Ⅎ} b x$
78		nfv	$⊢ Ⅎ b ⟨y, x⟩ = ⟨y, x⟩$
79		nfsbc1v	$⊢ Ⅎ b \underset{˙}{[} x / b \underset{˙}{]} \underset{˙}{[} y / a \underset{˙}{]} φ$
80	78 79	nfan	$⊢ Ⅎ b (⟨y, x⟩ = ⟨y, x⟩ \land \underset{˙}{[} x / b \underset{˙}{]} \underset{˙}{[} y / a \underset{˙}{]} φ)$
81		opeq2	$⊢ b = x \to ⟨y, b⟩ = ⟨y, x⟩$
82	81	eqeq2d	$⊢ b = x \to (⟨y, x⟩ = ⟨y, b⟩ \leftrightarrow ⟨y, x⟩ = ⟨y, x⟩)$
83		sbceq1a	$⊢ b = x \to (\underset{˙}{[} y / a \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} x / b \underset{˙}{]} \underset{˙}{[} y / a \underset{˙}{]} φ)$
84	82 83	anbi12d	$⊢ b = x \to ((⟨y, x⟩ = ⟨y, b⟩ \land \underset{˙}{[} y / a \underset{˙}{]} φ) \leftrightarrow (⟨y, x⟩ = ⟨y, x⟩ \land \underset{˙}{[} x / b \underset{˙}{]} \underset{˙}{[} y / a \underset{˙}{]} φ))$
85	77 80 84	spcegf	$⊢ x \in X \to ((⟨y, x⟩ = ⟨y, x⟩ \land \underset{˙}{[} x / b \underset{˙}{]} \underset{˙}{[} y / a \underset{˙}{]} φ) \to \exists b (⟨y, x⟩ = ⟨y, b⟩ \land \underset{˙}{[} y / a \underset{˙}{]} φ))$
86	45 76 85	sylc	$⊢ (([a ⇄ b] φ \land (x \in X \land y \in X)) \land (⟨x, y⟩ = ⟨a, b⟩ \land φ)) \to \exists b (⟨y, x⟩ = ⟨y, b⟩ \land \underset{˙}{[} y / a \underset{˙}{]} φ)$
87		nfcv	$⊢ \underline{Ⅎ} a y$
88		nfv	$⊢ Ⅎ a ⟨y, x⟩ = ⟨y, b⟩$
89		nfsbc1v	$⊢ Ⅎ a \underset{˙}{[} y / a \underset{˙}{]} φ$
90	88 89	nfan	$⊢ Ⅎ a (⟨y, x⟩ = ⟨y, b⟩ \land \underset{˙}{[} y / a \underset{˙}{]} φ)$
91	90	nfex	$⊢ Ⅎ a \exists b (⟨y, x⟩ = ⟨y, b⟩ \land \underset{˙}{[} y / a \underset{˙}{]} φ)$
92		opeq1	$⊢ a = y \to ⟨a, b⟩ = ⟨y, b⟩$
93	92	eqeq2d	$⊢ a = y \to (⟨y, x⟩ = ⟨a, b⟩ \leftrightarrow ⟨y, x⟩ = ⟨y, b⟩)$
94		sbceq1a	$⊢ a = y \to (φ \leftrightarrow \underset{˙}{[} y / a \underset{˙}{]} φ)$
95	93 94	anbi12d	$⊢ a = y \to ((⟨y, x⟩ = ⟨a, b⟩ \land φ) \leftrightarrow (⟨y, x⟩ = ⟨y, b⟩ \land \underset{˙}{[} y / a \underset{˙}{]} φ))$
96	95	exbidv	$⊢ a = y \to (\exists b (⟨y, x⟩ = ⟨a, b⟩ \land φ) \leftrightarrow \exists b (⟨y, x⟩ = ⟨y, b⟩ \land \underset{˙}{[} y / a \underset{˙}{]} φ))$
97	87 91 96	spcegf	$⊢ y \in X \to (\exists b (⟨y, x⟩ = ⟨y, b⟩ \land \underset{˙}{[} y / a \underset{˙}{]} φ) \to \exists a \exists b (⟨y, x⟩ = ⟨a, b⟩ \land φ))$
98	42 86 97	sylc	$⊢ (([a ⇄ b] φ \land (x \in X \land y \in X)) \land (⟨x, y⟩ = ⟨a, b⟩ \land φ)) \to \exists a \exists b (⟨y, x⟩ = ⟨a, b⟩ \land φ)$
99		simpl	$⊢ (y = x \land (x = a \land y = b)) \to y = x$
100		simprr	$⊢ (y = x \land (x = a \land y = b)) \to y = b$
101		simpl	$⊢ (x = a \land y = b) \to x = a$
102	101	adantl	$⊢ (y = x \land (x = a \land y = b)) \to x = a$
103	99 100 102	3eqtr3rd	$⊢ (y = x \land (x = a \land y = b)) \to a = b$
104	103	anim1i	$⊢ ((y = x \land (x = a \land y = b)) \land φ) \to (a = b \land φ)$
105	104	exp31	$⊢ y = x \to ((x = a \land y = b) \to (φ \to (a = b \land φ)))$
106	49 105	biimtrid	$⊢ y = x \to (⟨x, y⟩ = ⟨a, b⟩ \to (φ \to (a = b \land φ)))$
107	106	impd	$⊢ y = x \to ((⟨x, y⟩ = ⟨a, b⟩ \land φ) \to (a = b \land φ))$
108	48 47	opth1	$⊢ ⟨y, x⟩ = ⟨x, y⟩ \to y = x$
109	107 108	syl11	$⊢ (⟨x, y⟩ = ⟨a, b⟩ \land φ) \to (⟨y, x⟩ = ⟨x, y⟩ \to (a = b \land φ))$
110	109	adantl	$⊢ (([a ⇄ b] φ \land (x \in X \land y \in X)) \land (⟨x, y⟩ = ⟨a, b⟩ \land φ)) \to (⟨y, x⟩ = ⟨x, y⟩ \to (a = b \land φ))$
111	110	imp	$⊢ ((([a ⇄ b] φ \land (x \in X \land y \in X)) \land (⟨x, y⟩ = ⟨a, b⟩ \land φ)) \land ⟨y, x⟩ = ⟨x, y⟩) \to (a = b \land φ)$
112	111	19.8ad	$⊢ ((([a ⇄ b] φ \land (x \in X \land y \in X)) \land (⟨x, y⟩ = ⟨a, b⟩ \land φ)) \land ⟨y, x⟩ = ⟨x, y⟩) \to \exists b (a = b \land φ)$
113	112	19.8ad	$⊢ ((([a ⇄ b] φ \land (x \in X \land y \in X)) \land (⟨x, y⟩ = ⟨a, b⟩ \land φ)) \land ⟨y, x⟩ = ⟨x, y⟩) \to \exists a \exists b (a = b \land φ)$
114	113	ex	$⊢ (([a ⇄ b] φ \land (x \in X \land y \in X)) \land (⟨x, y⟩ = ⟨a, b⟩ \land φ)) \to (⟨y, x⟩ = ⟨x, y⟩ \to \exists a \exists b (a = b \land φ))$
115	98 114	embantd	$⊢ (([a ⇄ b] φ \land (x \in X \land y \in X)) \land (⟨x, y⟩ = ⟨a, b⟩ \land φ)) \to ((\exists a \exists b (⟨y, x⟩ = ⟨a, b⟩ \land φ) \to ⟨y, x⟩ = ⟨x, y⟩) \to \exists a \exists b (a = b \land φ))$
116	115	ex	$⊢ ([a ⇄ b] φ \land (x \in X \land y \in X)) \to ((⟨x, y⟩ = ⟨a, b⟩ \land φ) \to ((\exists a \exists b (⟨y, x⟩ = ⟨a, b⟩ \land φ) \to ⟨y, x⟩ = ⟨x, y⟩) \to \exists a \exists b (a = b \land φ)))$
117	40 116	syl5d	$⊢ ([a ⇄ b] φ \land (x \in X \land y \in X)) \to ((⟨x, y⟩ = ⟨a, b⟩ \land φ) \to (\forall v \in X \forall w \in X (\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \to ⟨v, w⟩ = ⟨x, y⟩) \to \exists a \exists b (a = b \land φ)))$
118	21 31 117	exlimd	$⊢ ([a ⇄ b] φ \land (x \in X \land y \in X)) \to (\exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \to (\forall v \in X \forall w \in X (\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \to ⟨v, w⟩ = ⟨x, y⟩) \to \exists a \exists b (a = b \land φ)))$
119	10 18 118	exlimd	$⊢ ([a ⇄ b] φ \land (x \in X \land y \in X)) \to (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \to (\forall v \in X \forall w \in X (\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \to ⟨v, w⟩ = ⟨x, y⟩) \to \exists a \exists b (a = b \land φ)))$
120	119	impd	$⊢ ([a ⇄ b] φ \land (x \in X \land y \in X)) \to ((\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall v \in X \forall w \in X (\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \to ⟨v, w⟩ = ⟨x, y⟩)) \to \exists a \exists b (a = b \land φ))$
121	120	rexlimdvva	$⊢ [a ⇄ b] φ \to (\exists x \in X \exists y \in X (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall v \in X \forall w \in X (\exists a \exists b (⟨v, w⟩ = ⟨a, b⟩ \land φ) \to ⟨v, w⟩ = ⟨x, y⟩)) \to \exists a \exists b (a = b \land φ))$
122	7 121	biimtrid	$⊢ [a ⇄ b] φ \to (\exists! p \in (X \times X) \exists a \exists b (p = ⟨a, b⟩ \land φ) \to \exists a \exists b (a = b \land φ))$

Metamath Proof Explorer

Theorem ichreuopeq

Proof