Theorem 2mo 2282

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.zE.wA.xA.y(ph -> (x = z /\ y = w)) <-> A.xA.yA.zA.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 1686	. . . . . . 7 |- (v = z -> (x = v <-> x = z))
2		equequ2 1686	. . . . . . 7 |- (u = w -> (y = u <-> y = w))
3	1, 2	bi2anan9 843	. . . . . 6 |- ((v = z /\ u = w) -> ((x = v /\ y = u) <-> (x = z /\ y = w)))
4	3	imbi2d 307	. . . . 5 |- ((v = z /\ u = w) -> ((ph -> (x = v /\ y = u)) <-> (ph -> (x = z /\ y = w))))
5	4	2albidv 1627	. . . 4 |- ((v = z /\ u = w) -> (A.xA.y(ph -> (x = v /\ y = u)) <-> A.xA.y(ph -> (x = z /\ y = w))))
6	5	cbvex2v 2007	. . 3 |- (E.vE.uA.xA.y(ph -> (x = v /\ y = u)) <-> E.zE.wA.xA.y(ph -> (x = z /\ y = w)))
7		nfv 1619	. . . . . . . . 9 |- F/z(ph -> (x = v /\ y = u))
8		nfv 1619	. . . . . . . . 9 |- F/w(ph -> (x = v /\ y = u))
9		nfs1v 2106	. . . . . . . . . 10 |- F/x[z / x][w / y]ph
10		nfv 1619	. . . . . . . . . 10 |- F/x(z = v /\ w = u)
11	9, 10	nfim 1813	. . . . . . . . 9 |- F/x([z / x][w / y]ph -> (z = v /\ w = u))
12		nfs1v 2106	. . . . . . . . . . 11 |- F/y[w / y]ph
13	12	nfsb 2109	. . . . . . . . . 10 |- F/y[z / x][w / y]ph
14		nfv 1619	. . . . . . . . . 10 |- F/y(z = v /\ w = u)
15	13, 14	nfim 1813	. . . . . . . . 9 |- F/y([z / x][w / y]ph -> (z = v /\ w = u))
16		sbequ12 1919	. . . . . . . . . . 11 |- (y = w -> (ph <-> [w / y]ph))
17		sbequ12 1919	. . . . . . . . . . 11 |- (x = z -> ([w / y]ph <-> [z / x][w / y]ph))
18	16, 17	sylan9bbr 681	. . . . . . . . . 10 |- ((x = z /\ y = w) -> (ph <-> [z / x][w / y]ph))
19		equequ1 1684	. . . . . . . . . . 11 |- (x = z -> (x = v <-> z = v))
20		equequ1 1684	. . . . . . . . . . 11 |- (y = w -> (y = u <-> w = u))
21	19, 20	bi2anan9 843	. . . . . . . . . 10 |- ((x = z /\ y = w) -> ((x = v /\ y = u) <-> (z = v /\ w = u)))
22	18, 21	imbi12d 311	. . . . . . . . 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 2004	. . . . . . . 8 |- (A.xA.y(ph -> (x = v /\ y = u)) <-> A.zA.w([z / x][w / y]ph -> (z = v /\ w = u)))
24	23	biimpi 186	. . . . . . 7 |- (A.xA.y(ph -> (x = v /\ y = u)) -> A.zA.w([z / x][w / y]ph -> (z = v /\ w = u)))
25	24	ancli 534	. . . . . 6 |- (A.xA.y(ph -> (x = v /\ y = u)) -> (A.xA.y(ph -> (x = v /\ y = u)) /\ A.zA.w([z / x][w / y]ph -> (z = v /\ w = u))))
26		alcom 1737	. . . . . . . . 9 |- (A.yA.zA.w((ph -> (x = v /\ y = u)) /\ ([z / x][w / y]ph -> (z = v /\ w = u))) <-> A.zA.yA.w((ph -> (x = v /\ y = u)) /\ ([z / x][w / y]ph -> (z = v /\ w = u))))
27	8, 15	aaan 1884	. . . . . . . . . 10 |- (A.yA.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 1566	. . . . . . . . 9 |- (A.zA.yA.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 240	. . . . . . . 8 |- (A.yA.zA.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 1566	. . . . . . 7 |- (A.xA.yA.zA.w((ph -> (x = v /\ y = u)) /\ ([z / x][w / y]ph -> (z = v /\ w = u))) <-> A.xA.z(A.y(ph -> (x = v /\ y = u)) /\ A.w([z / x][w / y]ph -> (z = v /\ w = u))))
31		nfv 1619	. . . . . . . 8 |- F/zA.y(ph -> (x = v /\ y = u))
32	11	nfal 1842	. . . . . . . 8 |- F/xA.w([z / x][w / y]ph -> (z = v /\ w = u))
33	31, 32	aaan 1884	. . . . . . 7 |- (A.xA.z(A.y(ph -> (x = v /\ y = u)) /\ A.w([z / x][w / y]ph -> (z = v /\ w = u))) <-> (A.xA.y(ph -> (x = v /\ y = u)) /\ A.zA.w([z / x][w / y]ph -> (z = v /\ w = u))))
34	30, 33	bitri 240	. . . . . 6 |- (A.xA.yA.zA.w((ph -> (x = v /\ y = u)) /\ ([z / x][w / y]ph -> (z = v /\ w = u))) <-> (A.xA.y(ph -> (x = v /\ y = u)) /\ A.zA.w([z / x][w / y]ph -> (z = v /\ w = u))))
35	25, 34	sylibr 203	. . . . 5 |- (A.xA.y(ph -> (x = v /\ y = u)) -> A.xA.yA.zA.w((ph -> (x = v /\ y = u)) /\ ([z / x][w / y]ph -> (z = v /\ w = u))))
36		prth 554	. . . . . . . 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 1688	. . . . . . . . . 10 |- ((x = v /\ z = v) -> x = z)
38		equtr2 1688	. . . . . . . . . 10 |- ((y = u /\ w = u) -> y = w)
39	37, 38	anim12i 549	. . . . . . . . 9 |- (((x = v /\ z = v) /\ (y = u /\ w = u)) -> (x = z /\ y = w))
40	39	an4s 799	. . . . . . . 8 |- (((x = v /\ y = u) /\ (z = v /\ w = u)) -> (x = z /\ y = w))
41	36, 40	syl6 29	. . . . . . 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 1560	. . . . . 6 |- (A.zA.w((ph -> (x = v /\ y = u)) /\ ([z / x][w / y]ph -> (z = v /\ w = u))) -> A.zA.w((ph /\ [z / x][w / y]ph) -> (x = z /\ y = w)))
43	42	2alimi 1560	. . . . 5 |- (A.xA.yA.zA.w((ph -> (x = v /\ y = u)) /\ ([z / x][w / y]ph -> (z = v /\ w = u))) -> A.xA.yA.zA.w((ph /\ [z / x][w / y]ph) -> (x = z /\ y = w)))
44	35, 43	syl 15	. . . 4 |- (A.xA.y(ph -> (x = v /\ y = u)) -> A.xA.yA.zA.w((ph /\ [z / x][w / y]ph) -> (x = z /\ y = w)))
45	44	exlimivv 1635	. . 3 |- (E.vE.uA.xA.y(ph -> (x = v /\ y = u)) -> A.xA.yA.zA.w((ph /\ [z / x][w / y]ph) -> (x = z /\ y = w)))
46	6, 45	sylbir 204	. 2 |- (E.zE.wA.xA.y(ph -> (x = z /\ y = w)) -> A.xA.yA.zA.w((ph /\ [z / x][w / y]ph) -> (x = z /\ y = w)))
47		alrot4 1739	. . . . 5 |- (A.xA.yA.zA.w((ph /\ [z / x][w / y]ph) -> (x = z /\ y = w)) <-> A.zA.wA.xA.y((ph /\ [z / x][w / y]ph) -> (x = z /\ y = w)))
48		pm3.21 435	. . . . . . . . . . . 12 |- ([z / x][w / y]ph -> (ph -> (ph /\ [z / x][w / y]ph)))
49	48	imim1d 69	. . . . . . . . . . 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 1764	. . . . . . . . . 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 1764	. . . . . . . . 9 |- ([z / x][w / y]ph -> (A.xA.y((ph /\ [z / x][w / y]ph) -> (x = z /\ y = w)) -> A.xA.y(ph -> (x = z /\ y = w))))
52	51	com12 27	. . . . . . . 8 |- (A.xA.y((ph /\ [z / x][w / y]ph) -> (x = z /\ y = w)) -> ([z / x][w / y]ph -> A.xA.y(ph -> (x = z /\ y = w))))
53	52	alimi 1559	. . . . . . 7 |- (A.wA.xA.y((ph /\ [z / x][w / y]ph) -> (x = z /\ y = w)) -> A.w([z / x][w / y]ph -> A.xA.y(ph -> (x = z /\ y = w))))
54		exim 1575	. . . . . . 7 |- (A.w([z / x][w / y]ph -> A.xA.y(ph -> (x = z /\ y = w))) -> (E.w[z / x][w / y]ph -> E.wA.xA.y(ph -> (x = z /\ y = w))))
55	53, 54	syl 15	. . . . . 6 |- (A.wA.xA.y((ph /\ [z / x][w / y]ph) -> (x = z /\ y = w)) -> (E.w[z / x][w / y]ph -> E.wA.xA.y(ph -> (x = z /\ y = w))))
56	55	alimi 1559	. . . . 5 |- (A.zA.wA.xA.y((ph /\ [z / x][w / y]ph) -> (x = z /\ y = w)) -> A.z(E.w[z / x][w / y]ph -> E.wA.xA.y(ph -> (x = z /\ y = w))))
57	47, 56	sylbi 187	. . . 4 |- (A.xA.yA.zA.w((ph /\ [z / x][w / y]ph) -> (x = z /\ y = w)) -> A.z(E.w[z / x][w / y]ph -> E.wA.xA.y(ph -> (x = z /\ y = w))))
58		exim 1575	. . . 4 |- (A.z(E.w[z / x][w / y]ph -> E.wA.xA.y(ph -> (x = z /\ y = w))) -> (E.zE.w[z / x][w / y]ph -> E.zE.wA.xA.y(ph -> (x = z /\ y = w))))
59	57, 58	syl 15	. . 3 |- (A.xA.yA.zA.w((ph /\ [z / x][w / y]ph) -> (x = z /\ y = w)) -> (E.zE.w[z / x][w / y]ph -> E.zE.wA.xA.y(ph -> (x = z /\ y = w))))
60		alnex 1543	. . . . . 6 |- (A.w -. [z / x][w / y]ph <-> -. E.w[z / x][w / y]ph)
61	60	albii 1566	. . . . 5 |- (A.zA.w -. [z / x][w / y]ph <-> A.z -. E.w[z / x][w / y]ph)
62		alnex 1543	. . . . 5 |- (A.z -. E.w[z / x][w / y]ph <-> -. E.zE.w[z / x][w / y]ph)
63	61, 62	bitri 240	. . . 4 |- (A.zA.w -. [z / x][w / y]ph <-> -. E.zE.w[z / x][w / y]ph)
64		nfv 1619	. . . . . . 7 |- F/z -. ph
65		nfv 1619	. . . . . . 7 |- F/w -. ph
66	9	nfn 1793	. . . . . . 7 |- F/x -. [z / x][w / y]ph
67	13	nfn 1793	. . . . . . 7 |- F/y -. [z / x][w / y]ph
68	18	notbid 285	. . . . . . 7 |- ((x = z /\ y = w) -> (-. ph <-> -. [z / x][w / y]ph))
69	64, 65, 66, 67, 68	cbval2 2004	. . . . . 6 |- (A.xA.y -. ph <-> A.zA.w -. [z / x][w / y]ph)
70		pm2.21 100	. . . . . . 7 |- (-. ph -> (ph -> (x = z /\ y = w)))
71	70	2alimi 1560	. . . . . 6 |- (A.xA.y -. ph -> A.xA.y(ph -> (x = z /\ y = w)))
72	69, 71	sylbir 204	. . . . 5 |- (A.zA.w -. [z / x][w / y]ph -> A.xA.y(ph -> (x = z /\ y = w)))
73		19.8a 1756	. . . . . 6 |- (E.wA.xA.y(ph -> (x = z /\ y = w)) -> E.zE.wA.xA.y(ph -> (x = z /\ y = w)))
74	73	19.23bi 1759	. . . . 5 |- (A.xA.y(ph -> (x = z /\ y = w)) -> E.zE.wA.xA.y(ph -> (x = z /\ y = w)))
75	72, 74	syl 15	. . . 4 |- (A.zA.w -. [z / x][w / y]ph -> E.zE.wA.xA.y(ph -> (x = z /\ y = w)))
76	63, 75	sylbir 204	. . 3 |- (-. E.zE.w[z / x][w / y]ph -> E.zE.wA.xA.y(ph -> (x = z /\ y = w)))
77	59, 76	pm2.61d1 151	. 2 |- (A.xA.yA.zA.w((ph /\ [z / x][w / y]ph) -> (x = z /\ y = w)) -> E.zE.wA.xA.y(ph -> (x = z /\ y = w)))
78	46, 77	impbii 180	1 |- (E.zE.wA.xA.y(ph -> (x = z /\ y = w)) <-> A.xA.yA.zA.w((ph /\ [z / x][w / y]ph) -> (x = z /\ y = w)))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   /\ wa 358  A.wal 1540  E.wex 1541   = 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:  2mos  2283  2eu6  2289