Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  2mo Structured version   Unicode version

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
Distinct variable groups:   ,,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem 2mo
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 equequ2 1742 . . . . . . 7
2 equequ2 1742 . . . . . . 7
31, 2bi2anan9 863 . . . . . 6
43imbi2d 316 . . . . 5
542albidv 1686 . . . 4
65cbvex2v 1984 . . 3
7 nfv 1678 . . . . . . . . 9
8 nfv 1678 . . . . . . . . 9
9 nfs1v 2147 . . . . . . . . . 10
10 nfv 1678 . . . . . . . . . 10
119, 10nfim 1857 . . . . . . . . 9
12 nfs1v 2147 . . . . . . . . . . 11
1312nfsb 2151 . . . . . . . . . 10
14 nfv 1678 . . . . . . . . . 10
1513, 14nfim 1857 . . . . . . . . 9
16 sbequ12 1941 . . . . . . . . . . 11
17 sbequ12 1941 . . . . . . . . . . 11
1816, 17sylan9bbr 695 . . . . . . . . . 10
19 equequ1 1741 . . . . . . . . . . 11
20 equequ1 1741 . . . . . . . . . . 11
2119, 20bi2anan9 863 . . . . . . . . . 10
2218, 21imbi12d 320 . . . . . . . . 9
237, 8, 11, 15, 22cbval2 1980 . . . . . . . 8
2423biimpi 194 . . . . . . 7
2524ancli 548 . . . . . 6
26 alcom 1788 . . . . . . . . 9
278, 15aaan 1907 . . . . . . . . . 10
2827albii 1615 . . . . . . . . 9
2926, 28bitri 249 . . . . . . . 8
3029albii 1615 . . . . . . 7
31 nfv 1678 . . . . . . . 8
3211nfal 1877 . . . . . . . 8
3331, 32aaan 1907 . . . . . . 7
3430, 33bitri 249 . . . . . 6
3525, 34sylibr 212 . . . . 5
36 prth 568 . . . . . . . 8
37 equtr2 1745 . . . . . . . . . 10
38 equtr2 1745 . . . . . . . . . 10
3937, 38anim12i 563 . . . . . . . . 9
4039an4s 817 . . . . . . . 8
4136, 40syl6 33 . . . . . . 7
42412alimi 1610 . . . . . 6
43422alimi 1610 . . . . 5
4435, 43syl 16 . . . 4
4544exlimivv 1694 . . 3
466, 45sylbir 213 . 2
47 alrot4 1790 . . . 4
48 pm3.21 446 . . . . . . . . . 10
4948imim1d 75 . . . . . . . . 9
5013, 49alimd 1815 . . . . . . . 8
519, 50alimd 1815 . . . . . . 7
5251com12 31 . . . . . 6
5352aleximi 1627 . . . . 5
5453aleximi 1627 . . . 4
5547, 54sylbi 195 . . 3
56 alnex 1593 . . . . . . 7
5756albii 1615 . . . . . 6
58 alnex 1593 . . . . . 6
5957, 58bitri 249 . . . . 5
60 nfv 1678 . . . . . 6
61 nfv 1678 . . . . . 6
6260, 61, 9, 13, 18cbvex2 1981 . . . . 5
6359, 62xchbinx 310 . . . 4
64 pm2.21 108 . . . . . . . 8
65642alimi 1610 . . . . . . 7
66652eximi 1631 . . . . . 6
676619.23bi 1810 . . . . 5
686719.23bi 1810 . . . 4
6963, 68sylbir 213 . . 3
7055, 69pm2.61d1 159 . 2
7146, 70impbii 188 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wa 369  wal 1362  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
 Copyright terms: Public domain W3C validator