Theorem mo 2226

Description: Equivalent definitions of "there exists at most one." (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)

Hypothesis

Ref	Expression
mo.1	|- F/yph

Assertion

Ref	Expression
mo	|- (E.yA.x(ph -> x = y) <-> A.xA.y((ph /\ [y / x]ph) -> x = y))

Distinct variable group:   x,y

Allowed substitution hints:   ph(x,y)

Proof of Theorem mo

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mo.1	. . . . . 6 |- F/yph
2		nfv 1619	. . . . . 6 |- F/y x = z
3	1, 2	nfim 1813	. . . . 5 |- F/y(ph -> x = z)
4	3	nfal 1842	. . . 4 |- F/yA.x(ph -> x = z)
5		nfv 1619	. . . 4 |- F/zA.x(ph -> x = y)
6		equequ2 1686	. . . . . 6 |- (z = y -> (x = z <-> x = y))
7	6	imbi2d 307	. . . . 5 |- (z = y -> ((ph -> x = z) <-> (ph -> x = y)))
8	7	albidv 1625	. . . 4 |- (z = y -> (A.x(ph -> x = z) <-> A.x(ph -> x = y)))
9	4, 5, 8	cbvex 1985	. . 3 |- (E.zA.x(ph -> x = z) <-> E.yA.x(ph -> x = y))
10	1	nfs1 2044	. . . . . . . . 9 |- F/x[y / x]ph
11		nfv 1619	. . . . . . . . 9 |- F/x y = z
12	10, 11	nfim 1813	. . . . . . . 8 |- F/x([y / x]ph -> y = z)
13		sbequ2 1650	. . . . . . . . 9 |- (x = y -> ([y / x]ph -> ph))
14		ax-8 1675	. . . . . . . . 9 |- (x = y -> (x = z -> y = z))
15	13, 14	imim12d 68	. . . . . . . 8 |- (x = y -> ((ph -> x = z) -> ([y / x]ph -> y = z)))
16	3, 12, 15	cbv3 1982	. . . . . . 7 |- (A.x(ph -> x = z) -> A.y([y / x]ph -> y = z))
17	16	ancli 534	. . . . . 6 |- (A.x(ph -> x = z) -> (A.x(ph -> x = z) /\ A.y([y / x]ph -> y = z)))
18	3, 12	aaan 1884	. . . . . 6 |- (A.xA.y((ph -> x = z) /\ ([y / x]ph -> y = z)) <-> (A.x(ph -> x = z) /\ A.y([y / x]ph -> y = z)))
19	17, 18	sylibr 203	. . . . 5 |- (A.x(ph -> x = z) -> A.xA.y((ph -> x = z) /\ ([y / x]ph -> y = z)))
20		prth 554	. . . . . . 7 |- (((ph -> x = z) /\ ([y / x]ph -> y = z)) -> ((ph /\ [y / x]ph) -> (x = z /\ y = z)))
21		equtr2 1688	. . . . . . 7 |- ((x = z /\ y = z) -> x = y)
22	20, 21	syl6 29	. . . . . 6 |- (((ph -> x = z) /\ ([y / x]ph -> y = z)) -> ((ph /\ [y / x]ph) -> x = y))
23	22	2alimi 1560	. . . . 5 |- (A.xA.y((ph -> x = z) /\ ([y / x]ph -> y = z)) -> A.xA.y((ph /\ [y / x]ph) -> x = y))
24	19, 23	syl 15	. . . 4 |- (A.x(ph -> x = z) -> A.xA.y((ph /\ [y / x]ph) -> x = y))
25	24	exlimiv 1634	. . 3 |- (E.zA.x(ph -> x = z) -> A.xA.y((ph /\ [y / x]ph) -> x = y))
26	9, 25	sylbir 204	. 2 |- (E.yA.x(ph -> x = y) -> A.xA.y((ph /\ [y / x]ph) -> x = y))
27		nfa2 1855	. . . 4 |- F/yA.xA.y((ph /\ [y / x]ph) -> x = y)
28		sp 1747	. . . . . . . 8 |- (A.y((ph /\ [y / x]ph) -> x = y) -> ((ph /\ [y / x]ph) -> x = y))
29	28	exp3a 425	. . . . . . 7 |- (A.y((ph /\ [y / x]ph) -> x = y) -> (ph -> ([y / x]ph -> x = y)))
30	29	com3r 73	. . . . . 6 |- ([y / x]ph -> (A.y((ph /\ [y / x]ph) -> x = y) -> (ph -> x = y)))
31	10, 30	alimd 1764	. . . . 5 |- ([y / x]ph -> (A.xA.y((ph /\ [y / x]ph) -> x = y) -> A.x(ph -> x = y)))
32	31	com12 27	. . . 4 |- (A.xA.y((ph /\ [y / x]ph) -> x = y) -> ([y / x]ph -> A.x(ph -> x = y)))
33	27, 32	eximd 1770	. . 3 |- (A.xA.y((ph /\ [y / x]ph) -> x = y) -> (E.y[y / x]ph -> E.yA.x(ph -> x = y)))
34		alnex 1543	. . . 4 |- (A.y -. [y / x]ph <-> -. E.y[y / x]ph)
35	10	nfn 1793	. . . . . 6 |- F/x -. [y / x]ph
36	1	nfn 1793	. . . . . 6 |- F/y -. ph
37		sbequ1 1918	. . . . . . . 8 |- (x = y -> (ph -> [y / x]ph))
38	37	equcoms 1681	. . . . . . 7 |- (y = x -> (ph -> [y / x]ph))
39	38	con3d 125	. . . . . 6 |- (y = x -> (-. [y / x]ph -> -. ph))
40	35, 36, 39	cbv3 1982	. . . . 5 |- (A.y -. [y / x]ph -> A.x -. ph)
41		pm2.21 100	. . . . . 6 |- (-. ph -> (ph -> x = y))
42	41	alimi 1559	. . . . 5 |- (A.x -. ph -> A.x(ph -> x = y))
43		19.8a 1756	. . . . 5 |- (A.x(ph -> x = y) -> E.yA.x(ph -> x = y))
44	40, 42, 43	3syl 18	. . . 4 |- (A.y -. [y / x]ph -> E.yA.x(ph -> x = y))
45	34, 44	sylbir 204	. . 3 |- (-. E.y[y / x]ph -> E.yA.x(ph -> x = y))
46	33, 45	pm2.61d1 151	. 2 |- (A.xA.y((ph /\ [y / x]ph) -> x = y) -> E.yA.x(ph -> x = y))
47	26, 46	impbii 180	1 |- (E.yA.x(ph -> x = y) <-> A.xA.y((ph /\ [y / x]ph) -> x = y))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   /\ wa 358  A.wal 1540  E.wex 1541   F/wnf 1544   = wceq 1642  [wsb 1648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649

This theorem is referenced by:  eu2  2229  eu3  2230  mo3  2235