![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > velsn | GIF version |
Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
velsn | ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 2644 | . 2 ⊢ 𝑥 ∈ V | |
2 | 1 | elsn 3490 | 1 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 = wceq 1299 ∈ wcel 1448 {csn 3474 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-tru 1302 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-v 2643 df-sn 3480 |
This theorem is referenced by: dfpr2 3493 mosn 3507 ralsnsg 3508 ralsns 3509 rexsns 3510 disjsn 3532 snprc 3535 euabsn2 3539 prmg 3591 snss 3596 difprsnss 3605 eqsnm 3629 snsssn 3635 snsspw 3638 dfnfc2 3701 uni0b 3708 uni0c 3709 sndisj 3871 unidif0 4031 exmid01 4061 rext 4075 exss 4087 frirrg 4210 ordsucim 4354 ordtriexmidlem 4373 ordtri2or2exmidlem 4379 onsucelsucexmidlem 4382 elirr 4394 sucprcreg 4402 fconstmpt 4524 opeliunxp 4532 dmsnopg 4946 dfmpt3 5181 nfunsn 5387 fsn 5524 fnasrn 5530 fnasrng 5532 fconstfvm 5570 eusvobj2 5692 opabex3d 5950 opabex3 5951 dcdifsnid 6330 ecexr 6364 ixp0x 6550 xpsnen 6644 fidifsnen 6693 difinfsn 6900 iccid 9549 fzsn 9687 fzpr 9698 fzdifsuc 9702 fsum2dlemstep 11042 ef0lem 11164 1nprm 11588 restsn 12131 |
Copyright terms: Public domain | W3C validator |