Theorem 2mo 2674

Description: Two ways of expressing "there exists at most one ordered pair ⟨𝑥, 𝑦⟩ such that 𝜑(𝑥, 𝑦) holds. See also 2mo2 2673. (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 2-Nov-2019.)

Assertion

Ref	Expression
2mo	⊢ (∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))

Distinct variable groups:   𝑥,𝑦,𝑧,𝑤   𝜑,𝑧,𝑤

Allowed substitution hints:   𝜑(𝑥, 𝑦)

Proof of Theorem 2mo

Step	Hyp	Ref	Expression
1		2mo2 2673	. . . 4 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) ↔ ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
2		nfmo1 2583	. . . . . . 7 ⊢ Ⅎ𝑥∃*𝑥∃𝑦𝜑
3		nfe1 2187	. . . . . . . 8 ⊢ Ⅎ𝑥∃𝑥𝜑
4	3	nfmov 2586	. . . . . . 7 ⊢ Ⅎ𝑥∃*𝑦∃𝑥𝜑
5	2, 4	nfan 1932	. . . . . 6 ⊢ Ⅎ𝑥(∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑)
6		nfe1 2187	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑦𝜑
7	6	nfmov 2586	. . . . . . . 8 ⊢ Ⅎ𝑦∃*𝑥∃𝑦𝜑
8		nfmo1 2583	. . . . . . . 8 ⊢ Ⅎ𝑦∃*𝑦∃𝑥𝜑
9	7, 8	nfan 1932	. . . . . . 7 ⊢ Ⅎ𝑦(∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑)
10		19.8a 2218	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑦𝜑)
11		spsbe 2119	. . . . . . . . . 10 ⊢ ([𝑤 / 𝑦]𝜑 → ∃𝑦𝜑)
12	11	sbimi 2111	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → [𝑧 / 𝑥]∃𝑦𝜑)
13		nfv 1947	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧∃𝑦𝜑
14	13	mo3 2590	. . . . . . . . . . 11 ⊢ (∃*𝑥∃𝑦𝜑 ↔ ∀𝑥∀𝑧((∃𝑦𝜑 ∧ [𝑧 / 𝑥]∃𝑦𝜑) → 𝑥 = 𝑧))
15	14	biimpi 219	. . . . . . . . . 10 ⊢ (∃*𝑥∃𝑦𝜑 → ∀𝑥∀𝑧((∃𝑦𝜑 ∧ [𝑧 / 𝑥]∃𝑦𝜑) → 𝑥 = 𝑧))
16	15	19.21bbi 2227	. . . . . . . . 9 ⊢ (∃*𝑥∃𝑦𝜑 → ((∃𝑦𝜑 ∧ [𝑧 / 𝑥]∃𝑦𝜑) → 𝑥 = 𝑧))
17	10, 12, 16	syl2ani 619	. . . . . . . 8 ⊢ (∃*𝑥∃𝑦𝜑 → ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → 𝑥 = 𝑧))
18		19.8a 2218	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑥𝜑)
19		sbcom2 2209	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑)
20		spsbe 2119	. . . . . . . . . . 11 ⊢ ([𝑧 / 𝑥]𝜑 → ∃𝑥𝜑)
21	20	sbimi 2111	. . . . . . . . . 10 ⊢ ([𝑤 / 𝑦][𝑧 / 𝑥]𝜑 → [𝑤 / 𝑦]∃𝑥𝜑)
22	19, 21	sylbi 220	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → [𝑤 / 𝑦]∃𝑥𝜑)
23		nfv 1947	. . . . . . . . . . . 12 ⊢ Ⅎ𝑤∃𝑥𝜑
24	23	mo3 2590	. . . . . . . . . . 11 ⊢ (∃*𝑦∃𝑥𝜑 ↔ ∀𝑦∀𝑤((∃𝑥𝜑 ∧ [𝑤 / 𝑦]∃𝑥𝜑) → 𝑦 = 𝑤))
25	24	biimpi 219	. . . . . . . . . 10 ⊢ (∃*𝑦∃𝑥𝜑 → ∀𝑦∀𝑤((∃𝑥𝜑 ∧ [𝑤 / 𝑦]∃𝑥𝜑) → 𝑦 = 𝑤))
26	25	19.21bbi 2227	. . . . . . . . 9 ⊢ (∃*𝑦∃𝑥𝜑 → ((∃𝑥𝜑 ∧ [𝑤 / 𝑦]∃𝑥𝜑) → 𝑦 = 𝑤))
27	18, 22, 26	syl2ani 619	. . . . . . . 8 ⊢ (∃*𝑦∃𝑥𝜑 → ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → 𝑦 = 𝑤))
28	17, 27	anim12ii 630	. . . . . . 7 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
29	9, 28	alrimi 2250	. . . . . 6 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
30	5, 29	alrimi 2250	. . . . 5 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
31	30	alrimivv 1961	. . . 4 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
32	1, 31	sylbir 238	. . 3 ⊢ (∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
33		nfs1v 2193	. . . . . . . 8 ⊢ Ⅎ𝑥[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
34		nfs1v 2193	. . . . . . . . . 10 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜑
35	34	nfsbv 2361	. . . . . . . . 9 ⊢ Ⅎ𝑦[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
36		pm3.21 477	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (𝜑 → (𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)))
37	36	imim1d 83	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
38	35, 37	alimd 2249	. . . . . . . 8 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
39	33, 38	alimd 2249	. . . . . . 7 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
40	39	com12 33	. . . . . 6 ⊢ (∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
41	40	aleximi 1865	. . . . 5 ⊢ (∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
42	41	aleximi 1865	. . . 4 ⊢ (∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
43		2nexaln 1863	. . . . . 6 ⊢ (¬ ∃𝑥∃𝑦𝜑 ↔ ∀𝑥∀𝑦 ¬ 𝜑)
44		nfv 1947	. . . . . . 7 ⊢ Ⅎ𝑤𝜑
45		nfv 1947	. . . . . . 7 ⊢ Ⅎ𝑧𝜑
46	44, 45	2sb8ef 2386	. . . . . 6 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
47	43, 46	xchnxbi 335	. . . . 5 ⊢ (¬ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦 ¬ 𝜑)
48		pm2.21 124	. . . . . . . . 9 ⊢ (¬ 𝜑 → (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
49	48	2alimi 1845	. . . . . . . 8 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
50	49	2eximi 1869	. . . . . . 7 ⊢ (∃𝑧∃𝑤∀𝑥∀𝑦 ¬ 𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
51	50	19.23bi 2228	. . . . . 6 ⊢ (∃𝑤∀𝑥∀𝑦 ¬ 𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
52	51	19.23bi 2228	. . . . 5 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
53	47, 52	sylbi 220	. . . 4 ⊢ (¬ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
54	42, 53	pm2.61d1 182	. . 3 ⊢ (∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
55	32, 54	impbii 212	. 2 ⊢ (∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
56		alrot4 2198	. 2 ⊢ (∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
57	55, 56	bitri 278	1 ⊢ (∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568  ∃wex 1812  [wsb 2099  ∃*wmo 2563

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2178  ax-11 2194  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565

This theorem is used by:  2mos  2675