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

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
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 1699 . . . . . . 7
2 equequ2 1699 . . . . . . 7
31, 2bi2anan9 845 . . . . . 6
43imbi2d 309 . . . . 5
542albidv 1638 . . . 4
65cbvex2v 1994 . . 3
7 nfv 1630 . . . . . . . . 9
8 nfv 1630 . . . . . . . . 9
9 nfs1v 2184 . . . . . . . . . 10
10 nfv 1630 . . . . . . . . . 10
119, 10nfim 1833 . . . . . . . . 9
12 nfs1v 2184 . . . . . . . . . . 11
1312nfsb 2187 . . . . . . . . . 10
14 nfv 1630 . . . . . . . . . 10
1513, 14nfim 1833 . . . . . . . . 9
16 sbequ12 1945 . . . . . . . . . . 11
17 sbequ12 1945 . . . . . . . . . . 11
1816, 17sylan9bbr 683 . . . . . . . . . 10
19 equequ1 1697 . . . . . . . . . . 11
20 equequ1 1697 . . . . . . . . . . 11
2119, 20bi2anan9 845 . . . . . . . . . 10
2218, 21imbi12d 313 . . . . . . . . 9
237, 8, 11, 15, 22cbval2 1990 . . . . . . . 8
2423biimpi 188 . . . . . . 7
2524ancli 536 . . . . . 6
26 alcom 1753 . . . . . . . . 9
278, 15aaan 1907 . . . . . . . . . 10
2827albii 1576 . . . . . . . . 9
2926, 28bitri 242 . . . . . . . 8
3029albii 1576 . . . . . . 7
31 nfv 1630 . . . . . . . 8
3211nfal 1865 . . . . . . . 8
3331, 32aaan 1907 . . . . . . 7
3430, 33bitri 242 . . . . . 6
3525, 34sylibr 205 . . . . 5
36 prth 556 . . . . . . . 8
37 equtr2 1701 . . . . . . . . . 10
38 equtr2 1701 . . . . . . . . . 10
3937, 38anim12i 551 . . . . . . . . 9
4039an4s 801 . . . . . . . 8
4136, 40syl6 32 . . . . . . 7
42412alimi 1570 . . . . . 6
43422alimi 1570 . . . . 5
4435, 43syl 16 . . . 4
4544exlimivv 1646 . . 3
466, 45sylbir 206 . 2
47 alrot4 1755 . . . . 5
48 pm3.21 437 . . . . . . . . . . . 12
4948imim1d 72 . . . . . . . . . . 11
5013, 49alimd 1781 . . . . . . . . . 10
519, 50alimd 1781 . . . . . . . . 9
5251com12 30 . . . . . . . 8
5352alimi 1569 . . . . . . 7
54 exim 1585 . . . . . . 7
5553, 54syl 16 . . . . . 6
5655alimi 1569 . . . . 5
5747, 56sylbi 189 . . . 4
58 exim 1585 . . . 4
5957, 58syl 16 . . 3
60 alnex 1553 . . . . . 6
6160albii 1576 . . . . 5
62 alnex 1553 . . . . 5
6361, 62bitri 242 . . . 4
64 nfv 1630 . . . . . . 7
65 nfv 1630 . . . . . . 7
669nfn 1812 . . . . . . 7
6713nfn 1812 . . . . . . 7
6818notbid 287 . . . . . . 7
6964, 65, 66, 67, 68cbval2 1990 . . . . . 6
70 pm2.21 103 . . . . . . 7
71702alimi 1570 . . . . . 6
7269, 71sylbir 206 . . . . 5
73 19.8a 1763 . . . . . 6
747319.23bi 1776 . . . . 5
7572, 74syl 16 . . . 4
7663, 75sylbir 206 . . 3
7759, 76pm2.61d1 154 . 2
7846, 77impbii 182 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wa 360  wal 1550  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
 Copyright terms: Public domain W3C validator