New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > elsnc | Unicode version |
Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.) |
Ref | Expression |
---|---|
elsnc.1 |
Ref | Expression |
---|---|
elsnc |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elsnc.1 | . 2 | |
2 | elsncg 3755 | . 2 | |
3 | 1, 2 | ax-mp 8 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 176 wceq 1642 wcel 1710 cvv 2859 csn 3737 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 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 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-v 2861 df-sn 3741 |
This theorem is referenced by: sneqr 3872 sniota 4369 nnsucelrlem1 4424 nnsucelrlem3 4426 nnsucelr 4428 nndisjeq 4429 ltfinex 4464 ltfintrilem1 4465 ssfin 4470 eqtfinrelk 4486 oddfinex 4504 evenoddnnnul 4514 evenodddisjlem1 4515 nnadjoinlem1 4519 vfinspss 4551 dfop2lem1 4573 setconslem2 4732 dmsnn0 5064 dmsnopg 5066 cnvsn 5073 rnsnop 5075 funsn 5147 iunfopab 5204 funconstss 5406 fsn 5432 fvclss 5462 1p1e2c 6155 fce 6188 dmfrec 6316 |
Copyright terms: Public domain | W3C validator |