reuopreuprim

Description: There is a unique unordered pair with ordered elements fulfilling a wff if there is a unique ordered pair fulfilling the wff. (Contributed by AV, 28-Jul-2023)

		Ref	Expression
	Assertion	reuopreuprim	$⊢ X \in V \to (\exists! p \in (X \times X) \exists a \exists b (p = ⟨a, b⟩ \land φ) \to \exists! p \in Pairs (X) \exists a \exists b (p = \{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 = ⟨i, j⟩ \to (p = ⟨a, b⟩ \leftrightarrow ⟨i, j⟩ = ⟨a, b⟩)$
5	4	anbi1d	$⊢ p = ⟨i, j⟩ \to ((p = ⟨a, b⟩ \land φ) \leftrightarrow (⟨i, j⟩ = ⟨a, b⟩ \land φ))$
6	5	2exbidv	$⊢ p = ⟨i, j⟩ \to (\exists a \exists b (p = ⟨a, b⟩ \land φ) \leftrightarrow \exists a \exists b (⟨i, j⟩ = ⟨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 i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩))$
8		simpll	$⊢ ((x \in X \land y \in X) \land (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩))) \to x \in X$
9		simplr	$⊢ ((x \in X \land y \in X) \land (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩))) \to y \in X$
10		oppr	$⊢ (x \in V \land y \in V) \to (⟨x, y⟩ = ⟨a, b⟩ \to \{x, y\} = \{a, b\})$
11	10	el2v	$⊢ ⟨x, y⟩ = ⟨a, b⟩ \to \{x, y\} = \{a, b\}$
12	11	anim1i	$⊢ (⟨x, y⟩ = ⟨a, b⟩ \land φ) \to (\{x, y\} = \{a, b\} \land φ)$
13	12	2eximi	$⊢ \exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \to \exists a \exists b (\{x, y\} = \{a, b\} \land φ)$
14	13	adantr	$⊢ (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩)) \to \exists a \exists b (\{x, y\} = \{a, b\} \land φ)$
15	14	adantl	$⊢ ((x \in X \land y \in X) \land (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩))) \to \exists a \exists b (\{x, y\} = \{a, b\} \land φ)$
16		nfv	$⊢ Ⅎ a (x \in X \land y \in X)$
17		nfe1	$⊢ Ⅎ a \exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ)$
18		nfcv	$⊢ \underline{Ⅎ} a X$
19		nfe1	$⊢ Ⅎ a \exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ)$
20		nfv	$⊢ Ⅎ a ⟨i, j⟩ = ⟨x, y⟩$
21	19 20	nfim	$⊢ Ⅎ a (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩)$
22	18 21	nfralw	$⊢ Ⅎ a \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩)$
23	18 22	nfralw	$⊢ Ⅎ a \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩)$
24	17 23	nfan	$⊢ Ⅎ a (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩))$
25	16 24	nfan	$⊢ Ⅎ a ((x \in X \land y \in X) \land (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩)))$
26		nfv	$⊢ Ⅎ a (m \in X \land n \in X)$
27	25 26	nfan	$⊢ Ⅎ a (((x \in X \land y \in X) \land (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩))) \land (m \in X \land n \in X))$
28		nfv	$⊢ Ⅎ a \{m, n\} = \{x, y\}$
29		nfv	$⊢ Ⅎ b (x \in X \land y \in X)$
30		nfe1	$⊢ Ⅎ b \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ)$
31	30	nfex	$⊢ Ⅎ b \exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ)$
32		nfcv	$⊢ \underline{Ⅎ} b X$
33		nfe1	$⊢ Ⅎ b \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ)$
34	33	nfex	$⊢ Ⅎ b \exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ)$
35		nfv	$⊢ Ⅎ b ⟨i, j⟩ = ⟨x, y⟩$
36	34 35	nfim	$⊢ Ⅎ b (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩)$
37	32 36	nfralw	$⊢ Ⅎ b \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩)$
38	32 37	nfralw	$⊢ Ⅎ b \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩)$
39	31 38	nfan	$⊢ Ⅎ b (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩))$
40	29 39	nfan	$⊢ Ⅎ b ((x \in X \land y \in X) \land (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩)))$
41		nfv	$⊢ Ⅎ b (m \in X \land n \in X)$
42	40 41	nfan	$⊢ Ⅎ b (((x \in X \land y \in X) \land (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩))) \land (m \in X \land n \in X))$
43		nfv	$⊢ Ⅎ b \{m, n\} = \{x, y\}$
44		vex	$⊢ m \in V$
45		vex	$⊢ n \in V$
46		vex	$⊢ a \in V$
47		vex	$⊢ b \in V$
48	44 45 46 47	preq12b	$⊢ \{m, n\} = \{a, b\} \leftrightarrow ((m = a \land n = b) \lor (m = b \land n = a))$
49		opeq1	$⊢ i = m \to ⟨i, j⟩ = ⟨m, j⟩$
50	49	eqeq1d	$⊢ i = m \to (⟨i, j⟩ = ⟨a, b⟩ \leftrightarrow ⟨m, j⟩ = ⟨a, b⟩)$
51	50	anbi1d	$⊢ i = m \to ((⟨i, j⟩ = ⟨a, b⟩ \land φ) \leftrightarrow (⟨m, j⟩ = ⟨a, b⟩ \land φ))$
52	51	2exbidv	$⊢ i = m \to (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \leftrightarrow \exists a \exists b (⟨m, j⟩ = ⟨a, b⟩ \land φ))$
53	49	eqeq1d	$⊢ i = m \to (⟨i, j⟩ = ⟨x, y⟩ \leftrightarrow ⟨m, j⟩ = ⟨x, y⟩)$
54	52 53	imbi12d	$⊢ i = m \to ((\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩) \leftrightarrow (\exists a \exists b (⟨m, j⟩ = ⟨a, b⟩ \land φ) \to ⟨m, j⟩ = ⟨x, y⟩))$
55		opeq2	$⊢ j = n \to ⟨m, j⟩ = ⟨m, n⟩$
56	55	eqeq1d	$⊢ j = n \to (⟨m, j⟩ = ⟨a, b⟩ \leftrightarrow ⟨m, n⟩ = ⟨a, b⟩)$
57	56	anbi1d	$⊢ j = n \to ((⟨m, j⟩ = ⟨a, b⟩ \land φ) \leftrightarrow (⟨m, n⟩ = ⟨a, b⟩ \land φ))$
58	57	2exbidv	$⊢ j = n \to (\exists a \exists b (⟨m, j⟩ = ⟨a, b⟩ \land φ) \leftrightarrow \exists a \exists b (⟨m, n⟩ = ⟨a, b⟩ \land φ))$
59	55	eqeq1d	$⊢ j = n \to (⟨m, j⟩ = ⟨x, y⟩ \leftrightarrow ⟨m, n⟩ = ⟨x, y⟩)$
60	58 59	imbi12d	$⊢ j = n \to ((\exists a \exists b (⟨m, j⟩ = ⟨a, b⟩ \land φ) \to ⟨m, j⟩ = ⟨x, y⟩) \leftrightarrow (\exists a \exists b (⟨m, n⟩ = ⟨a, b⟩ \land φ) \to ⟨m, n⟩ = ⟨x, y⟩))$
61	54 60	rspc2v	$⊢ (m \in X \land n \in X) \to (\forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩) \to (\exists a \exists b (⟨m, n⟩ = ⟨a, b⟩ \land φ) \to ⟨m, n⟩ = ⟨x, y⟩))$
62		pm3.22	$⊢ ((m \in X \land n \in X) \land (x \in X \land y \in X)) \to ((x \in X \land y \in X) \land (m \in X \land n \in X))$
63	62	3adant2	$⊢ ((m \in X \land n \in X) \land (m = a \land n = b) \land (x \in X \land y \in X)) \to ((x \in X \land y \in X) \land (m \in X \land n \in X))$
64	63	adantr	$⊢ (((m \in X \land n \in X) \land (m = a \land n = b) \land (x \in X \land y \in X)) \land φ) \to ((x \in X \land y \in X) \land (m \in X \land n \in X))$
65		eqidd	$⊢ (((m \in X \land n \in X) \land (m = a \land n = b) \land (x \in X \land y \in X)) \land φ) \to ⟨m, n⟩ = ⟨m, n⟩$
66		sbceq1a	$⊢ a = m \to (φ \leftrightarrow \underset{˙}{[} m / a \underset{˙}{]} φ)$
67	66	equcoms	$⊢ m = a \to (φ \leftrightarrow \underset{˙}{[} m / a \underset{˙}{]} φ)$
68		sbceq1a	$⊢ b = n \to (\underset{˙}{[} m / a \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} n / b \underset{˙}{]} \underset{˙}{[} m / a \underset{˙}{]} φ)$
69	68	equcoms	$⊢ n = b \to (\underset{˙}{[} m / a \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} n / b \underset{˙}{]} \underset{˙}{[} m / a \underset{˙}{]} φ)$
70	67 69	sylan9bb	$⊢ (m = a \land n = b) \to (φ \leftrightarrow \underset{˙}{[} n / b \underset{˙}{]} \underset{˙}{[} m / a \underset{˙}{]} φ)$
71	70	3ad2ant2	$⊢ ((m \in X \land n \in X) \land (m = a \land n = b) \land (x \in X \land y \in X)) \to (φ \leftrightarrow \underset{˙}{[} n / b \underset{˙}{]} \underset{˙}{[} m / a \underset{˙}{]} φ)$
72	71	biimpa	$⊢ (((m \in X \land n \in X) \land (m = a \land n = b) \land (x \in X \land y \in X)) \land φ) \to \underset{˙}{[} n / b \underset{˙}{]} \underset{˙}{[} m / a \underset{˙}{]} φ$
73	64 65 72	jca32	$⊢ (((m \in X \land n \in X) \land (m = a \land n = b) \land (x \in X \land y \in X)) \land φ) \to (((x \in X \land y \in X) \land (m \in X \land n \in X)) \land (⟨m, n⟩ = ⟨m, n⟩ \land \underset{˙}{[} n / b \underset{˙}{]} \underset{˙}{[} m / a \underset{˙}{]} φ))$
74		nfv	$⊢ Ⅎ a ⟨m, n⟩ = ⟨m, n⟩$
75		nfcv	$⊢ \underline{Ⅎ} a n$
76		nfsbc1v	$⊢ Ⅎ a \underset{˙}{[} m / a \underset{˙}{]} φ$
77	75 76	nfsbcw	$⊢ Ⅎ a \underset{˙}{[} n / b \underset{˙}{]} \underset{˙}{[} m / a \underset{˙}{]} φ$
78	74 77	nfan	$⊢ Ⅎ a (⟨m, n⟩ = ⟨m, n⟩ \land \underset{˙}{[} n / b \underset{˙}{]} \underset{˙}{[} m / a \underset{˙}{]} φ)$
79		nfv	$⊢ Ⅎ b ⟨m, n⟩ = ⟨m, n⟩$
80		nfsbc1v	$⊢ Ⅎ b \underset{˙}{[} n / b \underset{˙}{]} \underset{˙}{[} m / a \underset{˙}{]} φ$
81	79 80	nfan	$⊢ Ⅎ b (⟨m, n⟩ = ⟨m, n⟩ \land \underset{˙}{[} n / b \underset{˙}{]} \underset{˙}{[} m / a \underset{˙}{]} φ)$
82		opeq12	$⊢ (a = m \land b = n) \to ⟨a, b⟩ = ⟨m, n⟩$
83	82	eqeq2d	$⊢ (a = m \land b = n) \to (⟨m, n⟩ = ⟨a, b⟩ \leftrightarrow ⟨m, n⟩ = ⟨m, n⟩)$
84	66 68	sylan9bb	$⊢ (a = m \land b = n) \to (φ \leftrightarrow \underset{˙}{[} n / b \underset{˙}{]} \underset{˙}{[} m / a \underset{˙}{]} φ)$
85	83 84	anbi12d	$⊢ (a = m \land b = n) \to ((⟨m, n⟩ = ⟨a, b⟩ \land φ) \leftrightarrow (⟨m, n⟩ = ⟨m, n⟩ \land \underset{˙}{[} n / b \underset{˙}{]} \underset{˙}{[} m / a \underset{˙}{]} φ))$
86	85	adantl	$⊢ ((x \in X \land y \in X) \land (a = m \land b = n)) \to ((⟨m, n⟩ = ⟨a, b⟩ \land φ) \leftrightarrow (⟨m, n⟩ = ⟨m, n⟩ \land \underset{˙}{[} n / b \underset{˙}{]} \underset{˙}{[} m / a \underset{˙}{]} φ))$
87	78 81 86	spc2ed	$⊢ ((x \in X \land y \in X) \land (m \in X \land n \in X)) \to ((⟨m, n⟩ = ⟨m, n⟩ \land \underset{˙}{[} n / b \underset{˙}{]} \underset{˙}{[} m / a \underset{˙}{]} φ) \to \exists a \exists b (⟨m, n⟩ = ⟨a, b⟩ \land φ))$
88	87	imp	$⊢ (((x \in X \land y \in X) \land (m \in X \land n \in X)) \land (⟨m, n⟩ = ⟨m, n⟩ \land \underset{˙}{[} n / b \underset{˙}{]} \underset{˙}{[} m / a \underset{˙}{]} φ)) \to \exists a \exists b (⟨m, n⟩ = ⟨a, b⟩ \land φ)$
89		pm2.27	$⊢ \exists a \exists b (⟨m, n⟩ = ⟨a, b⟩ \land φ) \to ((\exists a \exists b (⟨m, n⟩ = ⟨a, b⟩ \land φ) \to ⟨m, n⟩ = ⟨x, y⟩) \to ⟨m, n⟩ = ⟨x, y⟩)$
90	73 88 89	3syl	$⊢ (((m \in X \land n \in X) \land (m = a \land n = b) \land (x \in X \land y \in X)) \land φ) \to ((\exists a \exists b (⟨m, n⟩ = ⟨a, b⟩ \land φ) \to ⟨m, n⟩ = ⟨x, y⟩) \to ⟨m, n⟩ = ⟨x, y⟩)$
91		oppr	$⊢ (m \in V \land n \in V) \to (⟨m, n⟩ = ⟨x, y⟩ \to \{m, n\} = \{x, y\})$
92	91	el2v	$⊢ ⟨m, n⟩ = ⟨x, y⟩ \to \{m, n\} = \{x, y\}$
93	90 92	syl6	$⊢ (((m \in X \land n \in X) \land (m = a \land n = b) \land (x \in X \land y \in X)) \land φ) \to ((\exists a \exists b (⟨m, n⟩ = ⟨a, b⟩ \land φ) \to ⟨m, n⟩ = ⟨x, y⟩) \to \{m, n\} = \{x, y\})$
94	93	ex	$⊢ ((m \in X \land n \in X) \land (m = a \land n = b) \land (x \in X \land y \in X)) \to (φ \to ((\exists a \exists b (⟨m, n⟩ = ⟨a, b⟩ \land φ) \to ⟨m, n⟩ = ⟨x, y⟩) \to \{m, n\} = \{x, y\}))$
95	94	com23	$⊢ ((m \in X \land n \in X) \land (m = a \land n = b) \land (x \in X \land y \in X)) \to ((\exists a \exists b (⟨m, n⟩ = ⟨a, b⟩ \land φ) \to ⟨m, n⟩ = ⟨x, y⟩) \to (φ \to \{m, n\} = \{x, y\}))$
96	95	3exp	$⊢ (m \in X \land n \in X) \to ((m = a \land n = b) \to ((x \in X \land y \in X) \to ((\exists a \exists b (⟨m, n⟩ = ⟨a, b⟩ \land φ) \to ⟨m, n⟩ = ⟨x, y⟩) \to (φ \to \{m, n\} = \{x, y\}))))$
97	96	com24	$⊢ (m \in X \land n \in X) \to ((\exists a \exists b (⟨m, n⟩ = ⟨a, b⟩ \land φ) \to ⟨m, n⟩ = ⟨x, y⟩) \to ((x \in X \land y \in X) \to ((m = a \land n = b) \to (φ \to \{m, n\} = \{x, y\}))))$
98	61 97	syld	$⊢ (m \in X \land n \in X) \to (\forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩) \to ((x \in X \land y \in X) \to ((m = a \land n = b) \to (φ \to \{m, n\} = \{x, y\}))))$
99	98	com13	$⊢ (x \in X \land y \in X) \to (\forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩) \to ((m \in X \land n \in X) \to ((m = a \land n = b) \to (φ \to \{m, n\} = \{x, y\}))))$
100	99	a1d	$⊢ (x \in X \land y \in X) \to (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \to (\forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩) \to ((m \in X \land n \in X) \to ((m = a \land n = b) \to (φ \to \{m, n\} = \{x, y\})))))$
101	100	imp42	$⊢ (((x \in X \land y \in X) \land (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩))) \land (m \in X \land n \in X)) \to ((m = a \land n = b) \to (φ \to \{m, n\} = \{x, y\}))$
102		opeq1	$⊢ i = n \to ⟨i, j⟩ = ⟨n, j⟩$
103	102	eqeq1d	$⊢ i = n \to (⟨i, j⟩ = ⟨a, b⟩ \leftrightarrow ⟨n, j⟩ = ⟨a, b⟩)$
104	103	anbi1d	$⊢ i = n \to ((⟨i, j⟩ = ⟨a, b⟩ \land φ) \leftrightarrow (⟨n, j⟩ = ⟨a, b⟩ \land φ))$
105	104	2exbidv	$⊢ i = n \to (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \leftrightarrow \exists a \exists b (⟨n, j⟩ = ⟨a, b⟩ \land φ))$
106	102	eqeq1d	$⊢ i = n \to (⟨i, j⟩ = ⟨x, y⟩ \leftrightarrow ⟨n, j⟩ = ⟨x, y⟩)$
107	105 106	imbi12d	$⊢ i = n \to ((\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩) \leftrightarrow (\exists a \exists b (⟨n, j⟩ = ⟨a, b⟩ \land φ) \to ⟨n, j⟩ = ⟨x, y⟩))$
108		opeq2	$⊢ j = m \to ⟨n, j⟩ = ⟨n, m⟩$
109	108	eqeq1d	$⊢ j = m \to (⟨n, j⟩ = ⟨a, b⟩ \leftrightarrow ⟨n, m⟩ = ⟨a, b⟩)$
110	109	anbi1d	$⊢ j = m \to ((⟨n, j⟩ = ⟨a, b⟩ \land φ) \leftrightarrow (⟨n, m⟩ = ⟨a, b⟩ \land φ))$
111	110	2exbidv	$⊢ j = m \to (\exists a \exists b (⟨n, j⟩ = ⟨a, b⟩ \land φ) \leftrightarrow \exists a \exists b (⟨n, m⟩ = ⟨a, b⟩ \land φ))$
112	108	eqeq1d	$⊢ j = m \to (⟨n, j⟩ = ⟨x, y⟩ \leftrightarrow ⟨n, m⟩ = ⟨x, y⟩)$
113	111 112	imbi12d	$⊢ j = m \to ((\exists a \exists b (⟨n, j⟩ = ⟨a, b⟩ \land φ) \to ⟨n, j⟩ = ⟨x, y⟩) \leftrightarrow (\exists a \exists b (⟨n, m⟩ = ⟨a, b⟩ \land φ) \to ⟨n, m⟩ = ⟨x, y⟩))$
114	107 113	rspc2v	$⊢ (n \in X \land m \in X) \to (\forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩) \to (\exists a \exists b (⟨n, m⟩ = ⟨a, b⟩ \land φ) \to ⟨n, m⟩ = ⟨x, y⟩))$
115	114	ancoms	$⊢ (m \in X \land n \in X) \to (\forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩) \to (\exists a \exists b (⟨n, m⟩ = ⟨a, b⟩ \land φ) \to ⟨n, m⟩ = ⟨x, y⟩))$
116		pm3.22	$⊢ (m \in X \land n \in X) \to (n \in X \land m \in X)$
117	116	anim1ci	$⊢ ((m \in X \land n \in X) \land (x \in X \land y \in X)) \to ((x \in X \land y \in X) \land (n \in X \land m \in X))$
118	117	3adant2	$⊢ ((m \in X \land n \in X) \land (m = b \land n = a) \land (x \in X \land y \in X)) \to ((x \in X \land y \in X) \land (n \in X \land m \in X))$
119	118	adantr	$⊢ (((m \in X \land n \in X) \land (m = b \land n = a) \land (x \in X \land y \in X)) \land φ) \to ((x \in X \land y \in X) \land (n \in X \land m \in X))$
120		eqidd	$⊢ (((m \in X \land n \in X) \land (m = b \land n = a) \land (x \in X \land y \in X)) \land φ) \to ⟨n, m⟩ = ⟨n, m⟩$
121		sbceq1a	$⊢ b = m \to (φ \leftrightarrow \underset{˙}{[} m / b \underset{˙}{]} φ)$
122	121	equcoms	$⊢ m = b \to (φ \leftrightarrow \underset{˙}{[} m / b \underset{˙}{]} φ)$
123		sbceq1a	$⊢ a = n \to (\underset{˙}{[} m / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} n / a \underset{˙}{]} \underset{˙}{[} m / b \underset{˙}{]} φ)$
124	123	equcoms	$⊢ n = a \to (\underset{˙}{[} m / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} n / a \underset{˙}{]} \underset{˙}{[} m / b \underset{˙}{]} φ)$
125	122 124	sylan9bb	$⊢ (m = b \land n = a) \to (φ \leftrightarrow \underset{˙}{[} n / a \underset{˙}{]} \underset{˙}{[} m / b \underset{˙}{]} φ)$
126	125	3ad2ant2	$⊢ ((m \in X \land n \in X) \land (m = b \land n = a) \land (x \in X \land y \in X)) \to (φ \leftrightarrow \underset{˙}{[} n / a \underset{˙}{]} \underset{˙}{[} m / b \underset{˙}{]} φ)$
127	126	biimpa	$⊢ (((m \in X \land n \in X) \land (m = b \land n = a) \land (x \in X \land y \in X)) \land φ) \to \underset{˙}{[} n / a \underset{˙}{]} \underset{˙}{[} m / b \underset{˙}{]} φ$
128	119 120 127	jca32	$⊢ (((m \in X \land n \in X) \land (m = b \land n = a) \land (x \in X \land y \in X)) \land φ) \to (((x \in X \land y \in X) \land (n \in X \land m \in X)) \land (⟨n, m⟩ = ⟨n, m⟩ \land \underset{˙}{[} n / a \underset{˙}{]} \underset{˙}{[} m / b \underset{˙}{]} φ))$
129		nfv	$⊢ Ⅎ a ⟨n, m⟩ = ⟨n, m⟩$
130		nfsbc1v	$⊢ Ⅎ a \underset{˙}{[} n / a \underset{˙}{]} \underset{˙}{[} m / b \underset{˙}{]} φ$
131	129 130	nfan	$⊢ Ⅎ a (⟨n, m⟩ = ⟨n, m⟩ \land \underset{˙}{[} n / a \underset{˙}{]} \underset{˙}{[} m / b \underset{˙}{]} φ)$
132		nfv	$⊢ Ⅎ b ⟨n, m⟩ = ⟨n, m⟩$
133		nfcv	$⊢ \underline{Ⅎ} b n$
134		nfsbc1v	$⊢ Ⅎ b \underset{˙}{[} m / b \underset{˙}{]} φ$
135	133 134	nfsbcw	$⊢ Ⅎ b \underset{˙}{[} n / a \underset{˙}{]} \underset{˙}{[} m / b \underset{˙}{]} φ$
136	132 135	nfan	$⊢ Ⅎ b (⟨n, m⟩ = ⟨n, m⟩ \land \underset{˙}{[} n / a \underset{˙}{]} \underset{˙}{[} m / b \underset{˙}{]} φ)$
137		opeq12	$⊢ (a = n \land b = m) \to ⟨a, b⟩ = ⟨n, m⟩$
138	137	eqeq2d	$⊢ (a = n \land b = m) \to (⟨n, m⟩ = ⟨a, b⟩ \leftrightarrow ⟨n, m⟩ = ⟨n, m⟩)$
139	121 123	sylan9bbr	$⊢ (a = n \land b = m) \to (φ \leftrightarrow \underset{˙}{[} n / a \underset{˙}{]} \underset{˙}{[} m / b \underset{˙}{]} φ)$
140	138 139	anbi12d	$⊢ (a = n \land b = m) \to ((⟨n, m⟩ = ⟨a, b⟩ \land φ) \leftrightarrow (⟨n, m⟩ = ⟨n, m⟩ \land \underset{˙}{[} n / a \underset{˙}{]} \underset{˙}{[} m / b \underset{˙}{]} φ))$
141	140	adantl	$⊢ ((x \in X \land y \in X) \land (a = n \land b = m)) \to ((⟨n, m⟩ = ⟨a, b⟩ \land φ) \leftrightarrow (⟨n, m⟩ = ⟨n, m⟩ \land \underset{˙}{[} n / a \underset{˙}{]} \underset{˙}{[} m / b \underset{˙}{]} φ))$
142	131 136 141	spc2ed	$⊢ ((x \in X \land y \in X) \land (n \in X \land m \in X)) \to ((⟨n, m⟩ = ⟨n, m⟩ \land \underset{˙}{[} n / a \underset{˙}{]} \underset{˙}{[} m / b \underset{˙}{]} φ) \to \exists a \exists b (⟨n, m⟩ = ⟨a, b⟩ \land φ))$
143	142	imp	$⊢ (((x \in X \land y \in X) \land (n \in X \land m \in X)) \land (⟨n, m⟩ = ⟨n, m⟩ \land \underset{˙}{[} n / a \underset{˙}{]} \underset{˙}{[} m / b \underset{˙}{]} φ)) \to \exists a \exists b (⟨n, m⟩ = ⟨a, b⟩ \land φ)$
144		pm2.27	$⊢ \exists a \exists b (⟨n, m⟩ = ⟨a, b⟩ \land φ) \to ((\exists a \exists b (⟨n, m⟩ = ⟨a, b⟩ \land φ) \to ⟨n, m⟩ = ⟨x, y⟩) \to ⟨n, m⟩ = ⟨x, y⟩)$
145	128 143 144	3syl	$⊢ (((m \in X \land n \in X) \land (m = b \land n = a) \land (x \in X \land y \in X)) \land φ) \to ((\exists a \exists b (⟨n, m⟩ = ⟨a, b⟩ \land φ) \to ⟨n, m⟩ = ⟨x, y⟩) \to ⟨n, m⟩ = ⟨x, y⟩)$
146		prcom	$⊢ \{n, m\} = \{m, n\}$
147		oppr	$⊢ (n \in V \land m \in V) \to (⟨n, m⟩ = ⟨x, y⟩ \to \{n, m\} = \{x, y\})$
148	147	el2v	$⊢ ⟨n, m⟩ = ⟨x, y⟩ \to \{n, m\} = \{x, y\}$
149	146 148	eqtr3id	$⊢ ⟨n, m⟩ = ⟨x, y⟩ \to \{m, n\} = \{x, y\}$
150	145 149	syl6	$⊢ (((m \in X \land n \in X) \land (m = b \land n = a) \land (x \in X \land y \in X)) \land φ) \to ((\exists a \exists b (⟨n, m⟩ = ⟨a, b⟩ \land φ) \to ⟨n, m⟩ = ⟨x, y⟩) \to \{m, n\} = \{x, y\})$
151	150	ex	$⊢ ((m \in X \land n \in X) \land (m = b \land n = a) \land (x \in X \land y \in X)) \to (φ \to ((\exists a \exists b (⟨n, m⟩ = ⟨a, b⟩ \land φ) \to ⟨n, m⟩ = ⟨x, y⟩) \to \{m, n\} = \{x, y\}))$
152	151	com23	$⊢ ((m \in X \land n \in X) \land (m = b \land n = a) \land (x \in X \land y \in X)) \to ((\exists a \exists b (⟨n, m⟩ = ⟨a, b⟩ \land φ) \to ⟨n, m⟩ = ⟨x, y⟩) \to (φ \to \{m, n\} = \{x, y\}))$
153	152	3exp	$⊢ (m \in X \land n \in X) \to ((m = b \land n = a) \to ((x \in X \land y \in X) \to ((\exists a \exists b (⟨n, m⟩ = ⟨a, b⟩ \land φ) \to ⟨n, m⟩ = ⟨x, y⟩) \to (φ \to \{m, n\} = \{x, y\}))))$
154	153	com24	$⊢ (m \in X \land n \in X) \to ((\exists a \exists b (⟨n, m⟩ = ⟨a, b⟩ \land φ) \to ⟨n, m⟩ = ⟨x, y⟩) \to ((x \in X \land y \in X) \to ((m = b \land n = a) \to (φ \to \{m, n\} = \{x, y\}))))$
155	115 154	syld	$⊢ (m \in X \land n \in X) \to (\forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩) \to ((x \in X \land y \in X) \to ((m = b \land n = a) \to (φ \to \{m, n\} = \{x, y\}))))$
156	155	com13	$⊢ (x \in X \land y \in X) \to (\forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩) \to ((m \in X \land n \in X) \to ((m = b \land n = a) \to (φ \to \{m, n\} = \{x, y\}))))$
157	156	a1d	$⊢ (x \in X \land y \in X) \to (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \to (\forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩) \to ((m \in X \land n \in X) \to ((m = b \land n = a) \to (φ \to \{m, n\} = \{x, y\})))))$
158	157	imp42	$⊢ (((x \in X \land y \in X) \land (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩))) \land (m \in X \land n \in X)) \to ((m = b \land n = a) \to (φ \to \{m, n\} = \{x, y\}))$
159	101 158	jaod	$⊢ (((x \in X \land y \in X) \land (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩))) \land (m \in X \land n \in X)) \to (((m = a \land n = b) \lor (m = b \land n = a)) \to (φ \to \{m, n\} = \{x, y\}))$
160	48 159	syl5bi	$⊢ (((x \in X \land y \in X) \land (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩))) \land (m \in X \land n \in X)) \to (\{m, n\} = \{a, b\} \to (φ \to \{m, n\} = \{x, y\}))$
161	160	impd	$⊢ (((x \in X \land y \in X) \land (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩))) \land (m \in X \land n \in X)) \to ((\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{x, y\})$
162	42 43 161	exlimd	$⊢ (((x \in X \land y \in X) \land (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩))) \land (m \in X \land n \in X)) \to (\exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{x, y\})$
163	27 28 162	exlimd	$⊢ (((x \in X \land y \in X) \land (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩))) \land (m \in X \land n \in X)) \to (\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{x, y\})$
164	163	ralrimivva	$⊢ ((x \in X \land y \in X) \land (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩))) \to \forall m \in X \forall n \in X (\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{x, y\})$
165		preq1	$⊢ v = x \to \{v, w\} = \{x, w\}$
166	165	eqeq1d	$⊢ v = x \to (\{v, w\} = \{a, b\} \leftrightarrow \{x, w\} = \{a, b\})$
167	166	anbi1d	$⊢ v = x \to ((\{v, w\} = \{a, b\} \land φ) \leftrightarrow (\{x, w\} = \{a, b\} \land φ))$
168	167	2exbidv	$⊢ v = x \to (\exists a \exists b (\{v, w\} = \{a, b\} \land φ) \leftrightarrow \exists a \exists b (\{x, w\} = \{a, b\} \land φ))$
169	165	eqeq2d	$⊢ v = x \to (\{m, n\} = \{v, w\} \leftrightarrow \{m, n\} = \{x, w\})$
170	169	imbi2d	$⊢ v = x \to ((\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{v, w\}) \leftrightarrow (\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{x, w\}))$
171	170	2ralbidv	$⊢ v = x \to (\forall m \in X \forall n \in X (\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{v, w\}) \leftrightarrow \forall m \in X \forall n \in X (\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{x, w\}))$
172	168 171	anbi12d	$⊢ v = x \to ((\exists a \exists b (\{v, w\} = \{a, b\} \land φ) \land \forall m \in X \forall n \in X (\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{v, w\})) \leftrightarrow (\exists a \exists b (\{x, w\} = \{a, b\} \land φ) \land \forall m \in X \forall n \in X (\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{x, w\})))$
173		preq2	$⊢ w = y \to \{x, w\} = \{x, y\}$
174	173	eqeq1d	$⊢ w = y \to (\{x, w\} = \{a, b\} \leftrightarrow \{x, y\} = \{a, b\})$
175	174	anbi1d	$⊢ w = y \to ((\{x, w\} = \{a, b\} \land φ) \leftrightarrow (\{x, y\} = \{a, b\} \land φ))$
176	175	2exbidv	$⊢ w = y \to (\exists a \exists b (\{x, w\} = \{a, b\} \land φ) \leftrightarrow \exists a \exists b (\{x, y\} = \{a, b\} \land φ))$
177	173	eqeq2d	$⊢ w = y \to (\{m, n\} = \{x, w\} \leftrightarrow \{m, n\} = \{x, y\})$
178	177	imbi2d	$⊢ w = y \to ((\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{x, w\}) \leftrightarrow (\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{x, y\}))$
179	178	2ralbidv	$⊢ w = y \to (\forall m \in X \forall n \in X (\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{x, w\}) \leftrightarrow \forall m \in X \forall n \in X (\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{x, y\}))$
180	176 179	anbi12d	$⊢ w = y \to ((\exists a \exists b (\{x, w\} = \{a, b\} \land φ) \land \forall m \in X \forall n \in X (\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{x, w\})) \leftrightarrow (\exists a \exists b (\{x, y\} = \{a, b\} \land φ) \land \forall m \in X \forall n \in X (\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{x, y\})))$
181	172 180	rspc2ev	$⊢ (x \in X \land y \in X \land (\exists a \exists b (\{x, y\} = \{a, b\} \land φ) \land \forall m \in X \forall n \in X (\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{x, y\}))) \to \exists v \in X \exists w \in X (\exists a \exists b (\{v, w\} = \{a, b\} \land φ) \land \forall m \in X \forall n \in X (\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{v, w\}))$
182	8 9 15 164 181	syl112anc	$⊢ ((x \in X \land y \in X) \land (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩))) \to \exists v \in X \exists w \in X (\exists a \exists b (\{v, w\} = \{a, b\} \land φ) \land \forall m \in X \forall n \in X (\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{v, w\}))$
183	182	ex	$⊢ (x \in X \land y \in X) \to ((\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩)) \to \exists v \in X \exists w \in X (\exists a \exists b (\{v, w\} = \{a, b\} \land φ) \land \forall m \in X \forall n \in X (\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{v, w\})))$
184	183	rexlimivv	$⊢ \exists x \in X \exists y \in X (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩)) \to \exists v \in X \exists w \in X (\exists a \exists b (\{v, w\} = \{a, b\} \land φ) \land \forall m \in X \forall n \in X (\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{v, w\}))$
185		eqeq1	$⊢ p = \{v, w\} \to (p = \{a, b\} \leftrightarrow \{v, w\} = \{a, b\})$
186	185	anbi1d	$⊢ p = \{v, w\} \to ((p = \{a, b\} \land φ) \leftrightarrow (\{v, w\} = \{a, b\} \land φ))$
187	186	2exbidv	$⊢ p = \{v, w\} \to (\exists a \exists b (p = \{a, b\} \land φ) \leftrightarrow \exists a \exists b (\{v, w\} = \{a, b\} \land φ))$
188		eqeq1	$⊢ p = \{m, n\} \to (p = \{a, b\} \leftrightarrow \{m, n\} = \{a, b\})$
189	188	anbi1d	$⊢ p = \{m, n\} \to ((p = \{a, b\} \land φ) \leftrightarrow (\{m, n\} = \{a, b\} \land φ))$
190	189	2exbidv	$⊢ p = \{m, n\} \to (\exists a \exists b (p = \{a, b\} \land φ) \leftrightarrow \exists a \exists b (\{m, n\} = \{a, b\} \land φ))$
191	187 190	reupr	$⊢ X \in V \to (\exists! p \in Pairs (X) \exists a \exists b (p = \{a, b\} \land φ) \leftrightarrow \exists v \in X \exists w \in X (\exists a \exists b (\{v, w\} = \{a, b\} \land φ) \land \forall m \in X \forall n \in X (\exists a \exists b (\{m, n\} = \{a, b\} \land φ) \to \{m, n\} = \{v, w\})))$
192	184 191	syl5ibr	$⊢ X \in V \to (\exists x \in X \exists y \in X (\exists a \exists b (⟨x, y⟩ = ⟨a, b⟩ \land φ) \land \forall i \in X \forall j \in X (\exists a \exists b (⟨i, j⟩ = ⟨a, b⟩ \land φ) \to ⟨i, j⟩ = ⟨x, y⟩)) \to \exists! p \in Pairs (X) \exists a \exists b (p = \{a, b\} \land φ))$
193	7 192	syl5bi	$⊢ X \in V \to (\exists! p \in (X \times X) \exists a \exists b (p = ⟨a, b⟩ \land φ) \to \exists! p \in Pairs (X) \exists a \exists b (p = \{a, b\} \land φ))$

Metamath Proof Explorer

Theorem reuopreuprim

Proof