reuop

Description: There is a unique ordered pair fulfilling a wff iff there are uniquely two sets fulfilling a corresponding wff. (Contributed by AV, 23-Jun-2023)

	Ref	Expression
Hypotheses	reu3op.a	$⊢ p = ⟨a, b⟩ \to (ψ \leftrightarrow χ)$
	reuop.x	$⊢ p = ⟨x, y⟩ \to (ψ \leftrightarrow θ)$
Assertion	reuop	$⊢ \exists! p \in (X \times Y) ψ \leftrightarrow \exists a \in X \exists b \in Y (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩))$

Proof

Step	Hyp	Ref	Expression
1		reu3op.a	$⊢ p = ⟨a, b⟩ \to (ψ \leftrightarrow χ)$
2		reuop.x	$⊢ p = ⟨x, y⟩ \to (ψ \leftrightarrow θ)$
3		nfsbc1v	$⊢ Ⅎ p \underset{˙}{[} q / p \underset{˙}{]} ψ$
4		nfsbc1v	$⊢ Ⅎ p \underset{˙}{[} w / p \underset{˙}{]} ψ$
5		sbceq1a	$⊢ p = w \to (ψ \leftrightarrow \underset{˙}{[} w / p \underset{˙}{]} ψ)$
6		dfsbcq	$⊢ w = q \to (\underset{˙}{[} w / p \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} q / p \underset{˙}{]} ψ)$
7	3 4 5 6	reu8nf	$⊢ \exists! p \in (X \times Y) ψ \leftrightarrow \exists p \in (X \times Y) (ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q))$
8		elxp2	$⊢ p \in (X \times Y) \leftrightarrow \exists a \in X \exists b \in Y p = ⟨a, b⟩$
9	1	biimpcd	$⊢ ψ \to (p = ⟨a, b⟩ \to χ)$
10	9	adantr	$⊢ (ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q)) \to (p = ⟨a, b⟩ \to χ)$
11	10	adantr	$⊢ ((ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q)) \land (a \in X \land b \in Y)) \to (p = ⟨a, b⟩ \to χ)$
12	11	imp	$⊢ (((ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q)) \land (a \in X \land b \in Y)) \land p = ⟨a, b⟩) \to χ$
13		opelxpi	$⊢ (x \in X \land y \in Y) \to ⟨x, y⟩ \in (X \times Y)$
14		dfsbcq	$⊢ q = ⟨x, y⟩ \to (\underset{˙}{[} q / p \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} ⟨x, y⟩ / p \underset{˙}{]} ψ)$
15		eqeq2	$⊢ q = ⟨x, y⟩ \to (p = q \leftrightarrow p = ⟨x, y⟩)$
16	14 15	imbi12d	$⊢ q = ⟨x, y⟩ \to ((\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q) \leftrightarrow (\underset{˙}{[} ⟨x, y⟩ / p \underset{˙}{]} ψ \to p = ⟨x, y⟩))$
17	16	adantl	$⊢ ((x \in X \land y \in Y) \land q = ⟨x, y⟩) \to ((\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q) \leftrightarrow (\underset{˙}{[} ⟨x, y⟩ / p \underset{˙}{]} ψ \to p = ⟨x, y⟩))$
18	13 17	rspcdv	$⊢ (x \in X \land y \in Y) \to (\forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q) \to (\underset{˙}{[} ⟨x, y⟩ / p \underset{˙}{]} ψ \to p = ⟨x, y⟩))$
19	18	adantr	$⊢ ((x \in X \land y \in Y) \land ψ) \to (\forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q) \to (\underset{˙}{[} ⟨x, y⟩ / p \underset{˙}{]} ψ \to p = ⟨x, y⟩))$
20		opex	$⊢ ⟨x, y⟩ \in V$
21	20 2	sbcie	$⊢ \underset{˙}{[} ⟨x, y⟩ / p \underset{˙}{]} ψ \leftrightarrow θ$
22		pm2.27	$⊢ \underset{˙}{[} ⟨x, y⟩ / p \underset{˙}{]} ψ \to ((\underset{˙}{[} ⟨x, y⟩ / p \underset{˙}{]} ψ \to p = ⟨x, y⟩) \to p = ⟨x, y⟩)$
23	21 22	sylbir	$⊢ θ \to ((\underset{˙}{[} ⟨x, y⟩ / p \underset{˙}{]} ψ \to p = ⟨x, y⟩) \to p = ⟨x, y⟩)$
24		eqcom	$⊢ ⟨x, y⟩ = p \leftrightarrow p = ⟨x, y⟩$
25	23 24	imbitrrdi	$⊢ θ \to ((\underset{˙}{[} ⟨x, y⟩ / p \underset{˙}{]} ψ \to p = ⟨x, y⟩) \to ⟨x, y⟩ = p)$
26	25	com12	$⊢ (\underset{˙}{[} ⟨x, y⟩ / p \underset{˙}{]} ψ \to p = ⟨x, y⟩) \to (θ \to ⟨x, y⟩ = p)$
27		eqeq2	$⊢ ⟨a, b⟩ = p \to (⟨x, y⟩ = ⟨a, b⟩ \leftrightarrow ⟨x, y⟩ = p)$
28	27	eqcoms	$⊢ p = ⟨a, b⟩ \to (⟨x, y⟩ = ⟨a, b⟩ \leftrightarrow ⟨x, y⟩ = p)$
29	28	imbi2d	$⊢ p = ⟨a, b⟩ \to ((θ \to ⟨x, y⟩ = ⟨a, b⟩) \leftrightarrow (θ \to ⟨x, y⟩ = p))$
30	26 29	syl5ibrcom	$⊢ (\underset{˙}{[} ⟨x, y⟩ / p \underset{˙}{]} ψ \to p = ⟨x, y⟩) \to (p = ⟨a, b⟩ \to (θ \to ⟨x, y⟩ = ⟨a, b⟩))$
31	30	a1d	$⊢ (\underset{˙}{[} ⟨x, y⟩ / p \underset{˙}{]} ψ \to p = ⟨x, y⟩) \to ((a \in X \land b \in Y) \to (p = ⟨a, b⟩ \to (θ \to ⟨x, y⟩ = ⟨a, b⟩)))$
32	19 31	syl6	$⊢ ((x \in X \land y \in Y) \land ψ) \to (\forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q) \to ((a \in X \land b \in Y) \to (p = ⟨a, b⟩ \to (θ \to ⟨x, y⟩ = ⟨a, b⟩))))$
33	32	expimpd	$⊢ (x \in X \land y \in Y) \to ((ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q)) \to ((a \in X \land b \in Y) \to (p = ⟨a, b⟩ \to (θ \to ⟨x, y⟩ = ⟨a, b⟩))))$
34	33	imp4c	$⊢ (x \in X \land y \in Y) \to ((((ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q)) \land (a \in X \land b \in Y)) \land p = ⟨a, b⟩) \to (θ \to ⟨x, y⟩ = ⟨a, b⟩))$
35	34	impcom	$⊢ ((((ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q)) \land (a \in X \land b \in Y)) \land p = ⟨a, b⟩) \land (x \in X \land y \in Y)) \to (θ \to ⟨x, y⟩ = ⟨a, b⟩)$
36	35	ralrimivva	$⊢ (((ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q)) \land (a \in X \land b \in Y)) \land p = ⟨a, b⟩) \to \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩)$
37	12 36	jca	$⊢ (((ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q)) \land (a \in X \land b \in Y)) \land p = ⟨a, b⟩) \to (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩))$
38	37	ex	$⊢ ((ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q)) \land (a \in X \land b \in Y)) \to (p = ⟨a, b⟩ \to (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩)))$
39	38	reximdvva	$⊢ (ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q)) \to (\exists a \in X \exists b \in Y p = ⟨a, b⟩ \to \exists a \in X \exists b \in Y (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩)))$
40	39	com12	$⊢ \exists a \in X \exists b \in Y p = ⟨a, b⟩ \to ((ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q)) \to \exists a \in X \exists b \in Y (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩)))$
41	8 40	sylbi	$⊢ p \in (X \times Y) \to ((ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q)) \to \exists a \in X \exists b \in Y (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩)))$
42	41	rexlimiv	$⊢ \exists p \in (X \times Y) (ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q)) \to \exists a \in X \exists b \in Y (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩))$
43		opelxpi	$⊢ (a \in X \land b \in Y) \to ⟨a, b⟩ \in (X \times Y)$
44	43	adantr	$⊢ ((a \in X \land b \in Y) \land (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩))) \to ⟨a, b⟩ \in (X \times Y)$
45		simprl	$⊢ ((a \in X \land b \in Y) \land (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩))) \to χ$
46		nfsbc1v	$⊢ Ⅎ x \underset{˙}{[} c / x \underset{˙}{]} θ$
47		nfv	$⊢ Ⅎ x ⟨c, y⟩ = ⟨a, b⟩$
48	46 47	nfim	$⊢ Ⅎ x (\underset{˙}{[} c / x \underset{˙}{]} θ \to ⟨c, y⟩ = ⟨a, b⟩)$
49		nfsbc1v	$⊢ Ⅎ y \underset{˙}{[} d / y \underset{˙}{]} \underset{˙}{[} c / x \underset{˙}{]} θ$
50		nfv	$⊢ Ⅎ y ⟨c, d⟩ = ⟨a, b⟩$
51	49 50	nfim	$⊢ Ⅎ y (\underset{˙}{[} d / y \underset{˙}{]} \underset{˙}{[} c / x \underset{˙}{]} θ \to ⟨c, d⟩ = ⟨a, b⟩)$
52		sbceq1a	$⊢ x = c \to (θ \leftrightarrow \underset{˙}{[} c / x \underset{˙}{]} θ)$
53		opeq1	$⊢ x = c \to ⟨x, y⟩ = ⟨c, y⟩$
54	53	eqeq1d	$⊢ x = c \to (⟨x, y⟩ = ⟨a, b⟩ \leftrightarrow ⟨c, y⟩ = ⟨a, b⟩)$
55	52 54	imbi12d	$⊢ x = c \to ((θ \to ⟨x, y⟩ = ⟨a, b⟩) \leftrightarrow (\underset{˙}{[} c / x \underset{˙}{]} θ \to ⟨c, y⟩ = ⟨a, b⟩))$
56		sbceq1a	$⊢ y = d \to (\underset{˙}{[} c / x \underset{˙}{]} θ \leftrightarrow \underset{˙}{[} d / y \underset{˙}{]} \underset{˙}{[} c / x \underset{˙}{]} θ)$
57		opeq2	$⊢ y = d \to ⟨c, y⟩ = ⟨c, d⟩$
58	57	eqeq1d	$⊢ y = d \to (⟨c, y⟩ = ⟨a, b⟩ \leftrightarrow ⟨c, d⟩ = ⟨a, b⟩)$
59	56 58	imbi12d	$⊢ y = d \to ((\underset{˙}{[} c / x \underset{˙}{]} θ \to ⟨c, y⟩ = ⟨a, b⟩) \leftrightarrow (\underset{˙}{[} d / y \underset{˙}{]} \underset{˙}{[} c / x \underset{˙}{]} θ \to ⟨c, d⟩ = ⟨a, b⟩))$
60	48 51 55 59	rspc2	$⊢ (c \in X \land d \in Y) \to (\forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩) \to (\underset{˙}{[} d / y \underset{˙}{]} \underset{˙}{[} c / x \underset{˙}{]} θ \to ⟨c, d⟩ = ⟨a, b⟩))$
61	60	ad2antlr	$⊢ (((a \in X \land b \in Y) \land (c \in X \land d \in Y)) \land χ) \to (\forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩) \to (\underset{˙}{[} d / y \underset{˙}{]} \underset{˙}{[} c / x \underset{˙}{]} θ \to ⟨c, d⟩ = ⟨a, b⟩))$
62	2	sbcop	$⊢ \underset{˙}{[} d / y \underset{˙}{]} \underset{˙}{[} c / x \underset{˙}{]} θ \leftrightarrow \underset{˙}{[} ⟨c, d⟩ / p \underset{˙}{]} ψ$
63		pm2.27	$⊢ \underset{˙}{[} d / y \underset{˙}{]} \underset{˙}{[} c / x \underset{˙}{]} θ \to ((\underset{˙}{[} d / y \underset{˙}{]} \underset{˙}{[} c / x \underset{˙}{]} θ \to ⟨c, d⟩ = ⟨a, b⟩) \to ⟨c, d⟩ = ⟨a, b⟩)$
64	62 63	sylbir	$⊢ \underset{˙}{[} ⟨c, d⟩ / p \underset{˙}{]} ψ \to ((\underset{˙}{[} d / y \underset{˙}{]} \underset{˙}{[} c / x \underset{˙}{]} θ \to ⟨c, d⟩ = ⟨a, b⟩) \to ⟨c, d⟩ = ⟨a, b⟩)$
65		eqcom	$⊢ ⟨a, b⟩ = ⟨c, d⟩ \leftrightarrow ⟨c, d⟩ = ⟨a, b⟩$
66	64 65	imbitrrdi	$⊢ \underset{˙}{[} ⟨c, d⟩ / p \underset{˙}{]} ψ \to ((\underset{˙}{[} d / y \underset{˙}{]} \underset{˙}{[} c / x \underset{˙}{]} θ \to ⟨c, d⟩ = ⟨a, b⟩) \to ⟨a, b⟩ = ⟨c, d⟩)$
67	66	com12	$⊢ (\underset{˙}{[} d / y \underset{˙}{]} \underset{˙}{[} c / x \underset{˙}{]} θ \to ⟨c, d⟩ = ⟨a, b⟩) \to (\underset{˙}{[} ⟨c, d⟩ / p \underset{˙}{]} ψ \to ⟨a, b⟩ = ⟨c, d⟩)$
68	61 67	syl6	$⊢ (((a \in X \land b \in Y) \land (c \in X \land d \in Y)) \land χ) \to (\forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩) \to (\underset{˙}{[} ⟨c, d⟩ / p \underset{˙}{]} ψ \to ⟨a, b⟩ = ⟨c, d⟩))$
69	68	expimpd	$⊢ ((a \in X \land b \in Y) \land (c \in X \land d \in Y)) \to ((χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩)) \to (\underset{˙}{[} ⟨c, d⟩ / p \underset{˙}{]} ψ \to ⟨a, b⟩ = ⟨c, d⟩))$
70	69	expcom	$⊢ (c \in X \land d \in Y) \to ((a \in X \land b \in Y) \to ((χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩)) \to (\underset{˙}{[} ⟨c, d⟩ / p \underset{˙}{]} ψ \to ⟨a, b⟩ = ⟨c, d⟩)))$
71	70	impd	$⊢ (c \in X \land d \in Y) \to (((a \in X \land b \in Y) \land (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩))) \to (\underset{˙}{[} ⟨c, d⟩ / p \underset{˙}{]} ψ \to ⟨a, b⟩ = ⟨c, d⟩))$
72	71	impcom	$⊢ (((a \in X \land b \in Y) \land (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩))) \land (c \in X \land d \in Y)) \to (\underset{˙}{[} ⟨c, d⟩ / p \underset{˙}{]} ψ \to ⟨a, b⟩ = ⟨c, d⟩)$
73		dfsbcq	$⊢ q = ⟨c, d⟩ \to (\underset{˙}{[} q / p \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} ⟨c, d⟩ / p \underset{˙}{]} ψ)$
74		eqeq2	$⊢ q = ⟨c, d⟩ \to (⟨a, b⟩ = q \leftrightarrow ⟨a, b⟩ = ⟨c, d⟩)$
75	73 74	imbi12d	$⊢ q = ⟨c, d⟩ \to ((\underset{˙}{[} q / p \underset{˙}{]} ψ \to ⟨a, b⟩ = q) \leftrightarrow (\underset{˙}{[} ⟨c, d⟩ / p \underset{˙}{]} ψ \to ⟨a, b⟩ = ⟨c, d⟩))$
76	72 75	syl5ibrcom	$⊢ (((a \in X \land b \in Y) \land (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩))) \land (c \in X \land d \in Y)) \to (q = ⟨c, d⟩ \to (\underset{˙}{[} q / p \underset{˙}{]} ψ \to ⟨a, b⟩ = q))$
77	76	rexlimdvva	$⊢ ((a \in X \land b \in Y) \land (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩))) \to (\exists c \in X \exists d \in Y q = ⟨c, d⟩ \to (\underset{˙}{[} q / p \underset{˙}{]} ψ \to ⟨a, b⟩ = q))$
78		elxp2	$⊢ q \in (X \times Y) \leftrightarrow \exists c \in X \exists d \in Y q = ⟨c, d⟩$
79	78	biimpi	$⊢ q \in (X \times Y) \to \exists c \in X \exists d \in Y q = ⟨c, d⟩$
80	77 79	impel	$⊢ (((a \in X \land b \in Y) \land (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩))) \land q \in (X \times Y)) \to (\underset{˙}{[} q / p \underset{˙}{]} ψ \to ⟨a, b⟩ = q)$
81	80	ralrimiva	$⊢ ((a \in X \land b \in Y) \land (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩))) \to \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to ⟨a, b⟩ = q)$
82		nfv	$⊢ Ⅎ p χ$
83		nfcv	$⊢ \underline{Ⅎ} p (X \times Y)$
84		nfv	$⊢ Ⅎ p ⟨a, b⟩ = q$
85	3 84	nfim	$⊢ Ⅎ p (\underset{˙}{[} q / p \underset{˙}{]} ψ \to ⟨a, b⟩ = q)$
86	83 85	nfralw	$⊢ Ⅎ p \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to ⟨a, b⟩ = q)$
87	82 86	nfan	$⊢ Ⅎ p (χ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to ⟨a, b⟩ = q))$
88		eqeq1	$⊢ p = ⟨a, b⟩ \to (p = q \leftrightarrow ⟨a, b⟩ = q)$
89	88	imbi2d	$⊢ p = ⟨a, b⟩ \to ((\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q) \leftrightarrow (\underset{˙}{[} q / p \underset{˙}{]} ψ \to ⟨a, b⟩ = q))$
90	89	ralbidv	$⊢ p = ⟨a, b⟩ \to (\forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q) \leftrightarrow \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to ⟨a, b⟩ = q))$
91	1 90	anbi12d	$⊢ p = ⟨a, b⟩ \to ((ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q)) \leftrightarrow (χ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to ⟨a, b⟩ = q)))$
92	87 91	rspce	$⊢ (⟨a, b⟩ \in (X \times Y) \land (χ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to ⟨a, b⟩ = q))) \to \exists p \in (X \times Y) (ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q))$
93	44 45 81 92	syl12anc	$⊢ ((a \in X \land b \in Y) \land (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩))) \to \exists p \in (X \times Y) (ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q))$
94	93	ex	$⊢ (a \in X \land b \in Y) \to ((χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩)) \to \exists p \in (X \times Y) (ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q)))$
95	94	rexlimivv	$⊢ \exists a \in X \exists b \in Y (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩)) \to \exists p \in (X \times Y) (ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q))$
96	42 95	impbii	$⊢ \exists p \in (X \times Y) (ψ \land \forall q \in (X \times Y) (\underset{˙}{[} q / p \underset{˙}{]} ψ \to p = q)) \leftrightarrow \exists a \in X \exists b \in Y (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩))$
97	7 96	bitri	$⊢ \exists! p \in (X \times Y) ψ \leftrightarrow \exists a \in X \exists b \in Y (χ \land \forall x \in X \forall y \in Y (θ \to ⟨x, y⟩ = ⟨a, b⟩))$

Metamath Proof Explorer

Theorem reuop

Proof