Theorem 2mo 2362

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

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 1742	. . . . . . 7 |- ( v = z -> ( x = v <-> x = z ) )
2		equequ2 1742	. . . . . . 7 |- ( u = w -> ( y = u <-> y = w ) )
3	1, 2	bi2anan9 863	. . . . . 6 |- ( ( v = z /\ u = w ) -> ( ( x = v /\ y = u ) <-> ( x = z /\ y = w ) ) )
4	3	imbi2d 316	. . . . 5 |- ( ( v = z /\ u = w ) -> ( ( ph -> ( x = v /\ y = u ) ) <-> ( ph -> ( x = z /\ y = w ) ) ) )
5	4	2albidv 1686	. . . 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 1984	. . 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 1678	. . . . . . . . 9 |- F/ z ( ph -> ( x = v /\ y = u ) )
8		nfv 1678	. . . . . . . . 9 |- F/ w ( ph -> ( x = v /\ y = u ) )
9		nfs1v 2147	. . . . . . . . . 10 |- F/ x [ z / x ] [ w / y ] ph
10		nfv 1678	. . . . . . . . . 10 |- F/ x ( z = v /\ w = u )
11	9, 10	nfim 1857	. . . . . . . . 9 |- F/ x ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) )
12		nfs1v 2147	. . . . . . . . . . 11 |- F/ y [ w / y ] ph
13	12	nfsb 2151	. . . . . . . . . 10 |- F/ y [ z / x ] [ w / y ] ph
14		nfv 1678	. . . . . . . . . 10 |- F/ y ( z = v /\ w = u )
15	13, 14	nfim 1857	. . . . . . . . 9 |- F/ y ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) )
16		sbequ12 1941	. . . . . . . . . . 11 |- ( y = w -> ( ph <-> [ w / y ] ph ) )
17		sbequ12 1941	. . . . . . . . . . 11 |- ( x = z -> ( [ w / y ] ph <-> [ z / x ] [ w / y ] ph ) )
18	16, 17	sylan9bbr 695	. . . . . . . . . 10 |- ( ( x = z /\ y = w ) -> ( ph <-> [ z / x ] [ w / y ] ph ) )
19		equequ1 1741	. . . . . . . . . . 11 |- ( x = z -> ( x = v <-> z = v ) )
20		equequ1 1741	. . . . . . . . . . 11 |- ( y = w -> ( y = u <-> w = u ) )
21	19, 20	bi2anan9 863	. . . . . . . . . 10 |- ( ( x = z /\ y = w ) -> ( ( x = v /\ y = u ) <-> ( z = v /\ w = u ) ) )
22	18, 21	imbi12d 320	. . . . . . . . 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 1980	. . . . . . . 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 194	. . . . . . 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 548	. . . . . 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 1788	. . . . . . . . 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 1907	. . . . . . . . . 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 1615	. . . . . . . . 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 249	. . . . . . . 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 1615	. . . . . . 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 1678	. . . . . . . 8 |- F/ z A. y ( ph -> ( x = v /\ y = u ) )
32	11	nfal 1877	. . . . . . . 8 |- F/ x A. w ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) )
33	31, 32	aaan 1907	. . . . . . 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 249	. . . . . 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 212	. . . . 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 568	. . . . . . . 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 1745	. . . . . . . . . 10 |- ( ( x = v /\ z = v ) -> x = z )
38		equtr2 1745	. . . . . . . . . 10 |- ( ( y = u /\ w = u ) -> y = w )
39	37, 38	anim12i 563	. . . . . . . . 9 |- ( ( ( x = v /\ z = v ) /\ ( y = u /\ w = u ) ) -> ( x = z /\ y = w ) )
40	39	an4s 817	. . . . . . . 8 |- ( ( ( x = v /\ y = u ) /\ ( z = v /\ w = u ) ) -> ( x = z /\ y = w ) )
41	36, 40	syl6 33	. . . . . . 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 1610	. . . . . 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 1610	. . . . 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 1694	. . 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 213	. 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 1790	. . . 4 |- ( 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 446	. . . . . . . . . 10 |- ( [ z / x ] [ w / y ] ph -> ( ph -> ( ph /\ [ z / x ] [ w / y ] ph ) ) )
49	48	imim1d 75	. . . . . . . . 9 |- ( [ z / x ] [ w / y ] ph -> ( ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) -> ( ph -> ( x = z /\ y = w ) ) ) )
50	13, 49	alimd 1815	. . . . . . . 8 |- ( [ 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 1815	. . . . . . 7 |- ( [ 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 31	. . . . . 6 |- ( 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	aleximi 1627	. . . . 5 |- ( 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 ) ) ) )
54	53	aleximi 1627	. . . 4 |- ( A. z A. w A. x A. y ( ( 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 ) ) ) )
55	47, 54	sylbi 195	. . 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 ) ) ) )
56		alnex 1593	. . . . . . 7 |- ( A. y -. ph <-> -. E. y ph )
57	56	albii 1615	. . . . . 6 |- ( A. x A. y -. ph <-> A. x -. E. y ph )
58		alnex 1593	. . . . . 6 |- ( A. x -. E. y ph <-> -. E. x E. y ph )
59	57, 58	bitri 249	. . . . 5 |- ( A. x A. y -. ph <-> -. E. x E. y ph )
60		nfv 1678	. . . . . 6 |- F/ z ph
61		nfv 1678	. . . . . 6 |- F/ w ph
62	60, 61, 9, 13, 18	cbvex2 1981	. . . . 5 |- ( E. x E. y ph <-> E. z E. w [ z / x ] [ w / y ] ph )
63	59, 62	xchbinx 310	. . . 4 |- ( A. x A. y -. ph <-> -. E. z E. w [ z / x ] [ w / y ] ph )
64		pm2.21 108	. . . . . . . 8 |- ( -. ph -> ( ph -> ( x = z /\ y = w ) ) )
65	64	2alimi 1610	. . . . . . 7 |- ( A. x A. y -. ph -> A. x A. y ( ph -> ( x = z /\ y = w ) ) )
66	65	2eximi 1631	. . . . . 6 |- ( E. z E. w A. x A. y -. ph -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
67	66	19.23bi 1810	. . . . 5 |- ( E. w A. x A. y -. ph -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
68	67	19.23bi 1810	. . . 4 |- ( A. x A. y -. ph -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
69	63, 68	sylbir 213	. . 3 |- ( -. E. z E. w [ z / x ] [ w / y ] ph -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
70	55, 69	pm2.61d1 159	. 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 ) ) )
71	46, 70	impbii 188	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 184   /\ wa 369   A.wal 1362   E.wex 1591   [wsb 1705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706

This theorem is referenced by:  2mos  2364  2eu6  2371