Theorem 2mo 2361

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 1699	. . . . . . 7 |- ( v = z -> ( x = v <-> x = z ) )
2		equequ2 1699	. . . . . . 7 |- ( u = w -> ( y = u <-> y = w ) )
3	1, 2	bi2anan9 845	. . . . . 6 |- ( ( v = z /\ u = w ) -> ( ( x = v /\ y = u ) <-> ( x = z /\ y = w ) ) )
4	3	imbi2d 309	. . . . 5 |- ( ( v = z /\ u = w ) -> ( ( ph -> ( x = v /\ y = u ) ) <-> ( ph -> ( x = z /\ y = w ) ) ) )
5	4	2albidv 1638	. . . 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 1994	. . 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 1630	. . . . . . . . 9 |- F/ z ( ph -> ( x = v /\ y = u ) )
8		nfv 1630	. . . . . . . . 9 |- F/ w ( ph -> ( x = v /\ y = u ) )
9		nfs1v 2184	. . . . . . . . . 10 |- F/ x [ z / x ] [ w / y ] ph
10		nfv 1630	. . . . . . . . . 10 |- F/ x ( z = v /\ w = u )
11	9, 10	nfim 1833	. . . . . . . . 9 |- F/ x ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) )
12		nfs1v 2184	. . . . . . . . . . 11 |- F/ y [ w / y ] ph
13	12	nfsb 2187	. . . . . . . . . 10 |- F/ y [ z / x ] [ w / y ] ph
14		nfv 1630	. . . . . . . . . 10 |- F/ y ( z = v /\ w = u )
15	13, 14	nfim 1833	. . . . . . . . 9 |- F/ y ( [ z / x ] [ w / y ] ph -> ( z = v /\ w = u ) )
16		sbequ12 1945	. . . . . . . . . . 11 |- ( y = w -> ( ph <-> [ w / y ] ph ) )
17		sbequ12 1945	. . . . . . . . . . 11 |- ( x = z -> ( [ w / y ] ph <-> [ z / x ] [ w / y ] ph ) )
18	16, 17	sylan9bbr 683	. . . . . . . . . 10 |- ( ( x = z /\ y = w ) -> ( ph <-> [ z / x ] [ w / y ] ph ) )
19		equequ1 1697	. . . . . . . . . . 11 |- ( x = z -> ( x = v <-> z = v ) )
20		equequ1 1697	. . . . . . . . . . 11 |- ( y = w -> ( y = u <-> w = u ) )
21	19, 20	bi2anan9 845	. . . . . . . . . 10 |- ( ( x = z /\ y = w ) -> ( ( x = v /\ y = u ) <-> ( z = v /\ w = u ) ) )
22	18, 21	imbi12d 313	. . . . . . . . 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 1990	. . . . . . . 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 188	. . . . . . 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 536	. . . . . 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 1753	. . . . . . . . 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 1576	. . . . . . . . 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 242	. . . . . . . 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 1576	. . . . . . 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 1630	. . . . . . . 8 |- F/ z A. y ( ph -> ( x = v /\ y = u ) )
32	11	nfal 1865	. . . . . . . 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 242	. . . . . 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 205	. . . . 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 556	. . . . . . . 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 1701	. . . . . . . . . 10 |- ( ( x = v /\ z = v ) -> x = z )
38		equtr2 1701	. . . . . . . . . 10 |- ( ( y = u /\ w = u ) -> y = w )
39	37, 38	anim12i 551	. . . . . . . . 9 |- ( ( ( x = v /\ z = v ) /\ ( y = u /\ w = u ) ) -> ( x = z /\ y = w ) )
40	39	an4s 801	. . . . . . . 8 |- ( ( ( x = v /\ y = u ) /\ ( z = v /\ w = u ) ) -> ( x = z /\ y = w ) )
41	36, 40	syl6 32	. . . . . . 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 1570	. . . . . 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 1570	. . . . 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 1646	. . 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 206	. 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 1755	. . . . 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 437	. . . . . . . . . . . 12 |- ( [ z / x ] [ w / y ] ph -> ( ph -> ( ph /\ [ z / x ] [ w / y ] ph ) ) )
49	48	imim1d 72	. . . . . . . . . . 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 1781	. . . . . . . . . 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 1781	. . . . . . . . 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 30	. . . . . . . 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 1569	. . . . . . 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 1585	. . . . . . 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 1569	. . . . 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 189	. . . 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 1585	. . . 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 1553	. . . . . 6 |- ( A. w -. [ z / x ] [ w / y ] ph <-> -. E. w [ z / x ] [ w / y ] ph )
61	60	albii 1576	. . . . 5 |- ( A. z A. w -. [ z / x ] [ w / y ] ph <-> A. z -. E. w [ z / x ] [ w / y ] ph )
62		alnex 1553	. . . . 5 |- ( A. z -. E. w [ z / x ] [ w / y ] ph <-> -. E. z E. w [ z / x ] [ w / y ] ph )
63	61, 62	bitri 242	. . . 4 |- ( A. z A. w -. [ z / x ] [ w / y ] ph <-> -. E. z E. w [ z / x ] [ w / y ] ph )
64		nfv 1630	. . . . . . 7 |- F/ z -. ph
65		nfv 1630	. . . . . . 7 |- F/ w -. ph
66	9	nfn 1812	. . . . . . 7 |- F/ x -. [ z / x ] [ w / y ] ph
67	13	nfn 1812	. . . . . . 7 |- F/ y -. [ z / x ] [ w / y ] ph
68	18	notbid 287	. . . . . . 7 |- ( ( x = z /\ y = w ) -> ( -. ph <-> -. [ z / x ] [ w / y ] ph ) )
69	64, 65, 66, 67, 68	cbval2 1990	. . . . . 6 |- ( A. x A. y -. ph <-> A. z A. w -. [ z / x ] [ w / y ] ph )
70		pm2.21 103	. . . . . . 7 |- ( -. ph -> ( ph -> ( x = z /\ y = w ) ) )
71	70	2alimi 1570	. . . . . 6 |- ( A. x A. y -. ph -> A. x A. y ( ph -> ( x = z /\ y = w ) ) )
72	69, 71	sylbir 206	. . . . 5 |- ( A. z A. w -. [ z / x ] [ w / y ] ph -> A. x A. y ( ph -> ( x = z /\ y = w ) ) )
73		19.8a 1763	. . . . . 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 1776	. . . . 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 206	. . 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 154	. 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 182	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 178   /\ wa 360   A.wal 1550   E.wex 1551   [wsb 1659

This theorem is referenced by:  2mos  2362  2eu6  2368

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951

This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660