Theorem 2mo 2340

Description: Two equivalent expressions for double "at most one." (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.)

Assertion

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

Distinct variable groups:   x, y, z, w   ph, z, w

Allowed substitution hints:   ph( x, y)

Proof of Theorem 2mo

Dummy variables v u are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		equequ2 1694	. . . . . . 7 |- ( v = z -> ( x = v <-> x = z ) )
2		equequ2 1694	. . . . . . 7 |- ( u = w -> ( y = u <-> y = w ) )
3	1, 2	bi2anan9 844	. . . . . 6 |- ( ( v = z /\ u = w ) -> ( ( x = v /\ y = u ) <-> ( x = z /\ y = w ) ) )
4	3	imbi2d 308	. . . . 5 |- ( ( v = z /\ u = w ) -> ( ( ph -> ( x = v /\ y = u ) ) <-> ( ph -> ( x = z /\ y = w ) ) ) )
5	4	2albidv 1634	. . . 4 |- ( ( v = z /\ u = w ) -> ( A. x A. y ( ph -> ( x = v /\ y = u ) ) <-> A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
6	5	cbvex2v 2069	. . 3 |- ( E. v E. u A. x A. y ( ph -> ( x = v /\ y = u ) ) <-> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
7		nfv 1626	. . . . . . . . 9 |- F/ z ( ph -> ( x = v /\ y = u ) )
8		nfv 1626	. . . . . . . . 9 |- F/ w ( ph -> ( x = v /\ y = u ) )
9		nfs1v 2163	. . . . . . . . . 10 |- F/ x [ z / x ] [ w / y ] ph
10		nfv 1626	. . . . . . . . . 10 |- F/ x ( z = v /\ w = u )
11	9, 10	nfim 1828	. . . . . . . . 9 |- F/ x ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) )
12		nfs1v 2163	. . . . . . . . . . 11 |- F/ y [ w / y ] ph
13	12	nfsb 2166	. . . . . . . . . 10 |- F/ y [ z / x ] [ w / y ] ph
14		nfv 1626	. . . . . . . . . 10 |- F/ y ( z = v /\ w = u )
15	13, 14	nfim 1828	. . . . . . . . 9 |- F/ y ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) )
16		sbequ12 1940	. . . . . . . . . . 11 |- ( y = w -> ( ph <-> [ w / y ] ph ) )
17		sbequ12 1940	. . . . . . . . . . 11 |- ( x = z -> ( [ w / y ] ph <-> [ z / x ] [ w / y ] ph ) )
18	16, 17	sylan9bbr 682	. . . . . . . . . 10 |- ( ( x = z /\ y = w ) -> ( ph <-> [ z / x ] [ w / y ] ph ) )
19		equequ1 1692	. . . . . . . . . . 11 |- ( x = z -> ( x = v <-> z = v ) )
20		equequ1 1692	. . . . . . . . . . 11 |- ( y = w -> ( y = u <-> w = u ) )
21	19, 20	bi2anan9 844	. . . . . . . . . 10 |- ( ( x = z /\ y = w ) -> ( ( x = v /\ y = u ) <-> ( z = v /\ w = u ) ) )
22	18, 21	imbi12d 312	. . . . . . . . 9 |- ( ( x = z /\ y = w ) -> ( ( ph -> ( x = v /\ y = u ) ) <-> ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) )
23	7, 8, 11, 15, 22	cbval2 2065	. . . . . . . 8 |- ( A. x A. y ( ph -> ( x = v /\ y = u ) ) <-> A. z A. w ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) )
24	23	biimpi 187	. . . . . . 7 |- ( A. x A. y ( ph -> ( x = v /\ y = u ) ) -> A. z A. w ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) )
25	24	ancli 535	. . . . . 6 |- ( A. x A. y ( ph -> ( x = v /\ y = u ) ) -> ( A. x A. y ( ph -> ( x = v /\ y = u ) ) /\ A. z A. w ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) )
26		alcom 1748	. . . . . . . . 9 |- ( A. y A. z A. w ( ( ph -> ( x = v /\ y = u ) ) /\ ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) <-> A. z A. y A. w ( ( ph -> ( x = v /\ y = u ) ) /\ ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) )
27	8, 15	aaan 1902	. . . . . . . . . 10 |- ( A. y A. w ( ( ph -> ( x = v /\ y = u ) ) /\ ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) <-> ( A. y ( ph -> ( x = v /\ y = u ) ) /\ A. w ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) )
28	27	albii 1572	. . . . . . . . 9 |- ( A. z A. y A. w ( ( ph -> ( x = v /\ y = u ) ) /\ ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) <-> A. z ( A. y ( ph -> ( x = v /\ y = u ) ) /\ A. w ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) )
29	26, 28	bitri 241	. . . . . . . 8 |- ( A. y A. z A. w ( ( ph -> ( x = v /\ y = u ) ) /\ ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) <-> A. z ( A. y ( ph -> ( x = v /\ y = u ) ) /\ A. w ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) )
30	29	albii 1572	. . . . . . 7 |- ( A. x A. y A. z A. w ( ( ph -> ( x = v /\ y = u ) ) /\ ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) <-> A. x A. z ( A. y ( ph -> ( x = v /\ y = u ) ) /\ A. w ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) )
31		nfv 1626	. . . . . . . 8 |- F/ z A. y ( ph -> ( x = v /\ y = u ) )
32	11	nfal 1860	. . . . . . . 8 |- F/ x A. w ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) )
33	31, 32	aaan 1902	. . . . . . 7 |- ( A. x A. z ( A. y ( ph -> ( x = v /\ y = u ) ) /\ A. w ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) <-> ( A. x A. y ( ph -> ( x = v /\ y = u ) ) /\ A. z A. w ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) )
34	30, 33	bitri 241	. . . . . 6 |- ( A. x A. y A. z A. w ( ( ph -> ( x = v /\ y = u ) ) /\ ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) <-> ( A. x A. y ( ph -> ( x = v /\ y = u ) ) /\ A. z A. w ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) )
35	25, 34	sylibr 204	. . . . 5 |- ( A. x A. y ( ph -> ( x = v /\ y = u ) ) -> A. x A. y A. z A. w ( ( ph -> ( x = v /\ y = u ) ) /\ ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) )
36		prth 555	. . . . . . . 8 |- ( ( ( ph -> ( x = v /\ y = u ) ) /\ ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) -> ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( ( x = v /\ y = u ) /\ ( z = v /\ w = u ) ) ) )
37		equtr2 1696	. . . . . . . . . 10 |- ( ( x = v /\ z = v ) -> x = z )
38		equtr2 1696	. . . . . . . . . 10 |- ( ( y = u /\ w = u ) -> y = w )
39	37, 38	anim12i 550	. . . . . . . . 9 |- ( ( ( x = v /\ z = v ) /\ ( y = u /\ w = u ) ) -> ( x = z /\ y = w ) )
40	39	an4s 800	. . . . . . . 8 |- ( ( ( x = v /\ y = u ) /\ ( z = v /\ w = u ) ) -> ( x = z /\ y = w ) )
41	36, 40	syl6 31	. . . . . . 7 |- ( ( ( ph -> ( x = v /\ y = u ) ) /\ ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) -> ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )
42	41	2alimi 1566	. . . . . 6 |- ( A. z A. w ( ( ph -> ( x = v /\ y = u ) ) /\ ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) -> A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )
43	42	2alimi 1566	. . . . 5 |- ( A. x A. y A. z A. w ( ( ph -> ( x = v /\ y = u ) ) /\ ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) ) ) -> A. x A. y A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )
44	35, 43	syl 16	. . . 4 |- ( A. x A. y ( ph -> ( x = v /\ y = u ) ) -> A. x A. y A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )
45	44	exlimivv 1642	. . 3 |- ( E. v E. u A. x A. y ( ph -> ( x = v /\ y = u ) ) -> A. x A. y A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )
46	6, 45	sylbir 205	. 2 |- ( E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) -> A. x A. y A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )
47		alrot4 1750	. . . . 5 |- ( A. x A. y A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) <-> A. z A. w A. x A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )
48		pm3.21 436	. . . . . . . . . . . 12 |- ( [ z / x ] [ w / y ] ph -> ( ph -> ( ph /\ [ z / x ] [ w / y ] ph ) ) )
49	48	imim1d 71	. . . . . . . . . . 11 |- ( [ z / x ] [ w / y ] ph -> ( ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) -> ( ph -> ( x = z /\ y = w ) ) ) )
50	13, 49	alimd 1776	. . . . . . . . . 10 |- ( [ z / x ] [ w / y ] ph -> ( A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) -> A. y ( ph -> ( x = z /\ y = w ) ) ) )
51	9, 50	alimd 1776	. . . . . . . . 9 |- ( [ z / x ] [ w / y ] ph -> ( A. x A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) -> A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
52	51	com12 29	. . . . . . . 8 |- ( A. x A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) -> ( [ z / x ] [ w / y ] ph -> A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
53	52	alimi 1565	. . . . . . 7 |- ( A. w A. x A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) -> A. w ( [ z / x ] [ w / y ] ph -> A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
54		exim 1581	. . . . . . 7 |- ( A. w ( [ z / x ] [ w / y ] ph -> A. x A. y ( ph -> ( x = z /\ y = w ) ) ) -> ( E. w [ z / x ] [ w / y ] ph -> E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
55	53, 54	syl 16	. . . . . 6 |- ( A. w A. x A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) -> ( E. w [ z / x ] [ w / y ] ph -> E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
56	55	alimi 1565	. . . . 5 |- ( A. z A. w A. x A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) -> A. z ( E. w [ z / x ] [ w / y ] ph -> E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
57	47, 56	sylbi 188	. . . 4 |- ( A. x A. y A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) -> A. z ( E. w [ z / x ] [ w / y ] ph -> E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
58		exim 1581	. . . 4 |- ( A. z ( E. w [ z / x ] [ w / y ] ph -> E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) -> ( E. z E. w [ z / x ] [ w / y ] ph -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
59	57, 58	syl 16	. . 3 |- ( A. x A. y A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) -> ( E. z E. w [ z / x ] [ w / y ] ph -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
60		alnex 1549	. . . . . 6 |- ( A. w -. [ z / x ] [ w / y ] ph <-> -. E. w [ z / x ] [ w / y ] ph )
61	60	albii 1572	. . . . 5 |- ( A. z A. w -. [ z / x ] [ w / y ] ph <-> A. z -. E. w [ z / x ] [ w / y ] ph )
62		alnex 1549	. . . . 5 |- ( A. z -. E. w [ z / x ] [ w / y ] ph <-> -. E. z E. w [ z / x ] [ w / y ] ph )
63	61, 62	bitri 241	. . . 4 |- ( A. z A. w -. [ z / x ] [ w / y ] ph <-> -. E. z E. w [ z / x ] [ w / y ] ph )
64		nfv 1626	. . . . . . 7 |- F/ z -. ph
65		nfv 1626	. . . . . . 7 |- F/ w -. ph
66	9	nfn 1807	. . . . . . 7 |- F/ x -. [ z / x ] [ w / y ] ph
67	13	nfn 1807	. . . . . . 7 |- F/ y -. [ z / x ] [ w / y ] ph
68	18	notbid 286	. . . . . . 7 |- ( ( x = z /\ y = w ) -> ( -. ph <-> -. [ z / x ] [ w / y ] ph ) )
69	64, 65, 66, 67, 68	cbval2 2065	. . . . . 6 |- ( A. x A. y -. ph <-> A. z A. w -. [ z / x ] [ w / y ] ph )
70		pm2.21 102	. . . . . . 7 |- ( -. ph -> ( ph -> ( x = z /\ y = w ) ) )
71	70	2alimi 1566	. . . . . 6 |- ( A. x A. y -. ph -> A. x A. y ( ph -> ( x = z /\ y = w ) ) )
72	69, 71	sylbir 205	. . . . 5 |- ( A. z A. w -. [ z / x ] [ w / y ] ph -> A. x A. y ( ph -> ( x = z /\ y = w ) ) )
73		19.8a 1758	. . . . . 6 |- ( E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
74	73	19.23bi 1771	. . . . 5 |- ( A. x A. y ( ph -> ( x = z /\ y = w ) ) -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
75	72, 74	syl 16	. . . 4 |- ( A. z A. w -. [ z / x ] [ w / y ] ph -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
76	63, 75	sylbir 205	. . 3 |- ( -. E. z E. w [ z / x ] [ w / y ] ph -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
77	59, 76	pm2.61d1 153	. 2 |- ( A. x A. y A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
78	46, 77	impbii 181	1 |- ( E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) <-> A. x A. y A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   /\ wa 359   A.wal 1546   E.wex 1547   [wsb 1655

This theorem is referenced by:  2mos  2341  2eu6  2347

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656