![]() |
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 2755 | . 2 ⊢ 𝑥 ∈ V | |
2 | 1 | elsn 3623 | 1 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 = wceq 1364 ∈ wcel 2160 {csn 3607 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 df-sn 3613 |
This theorem is referenced by: dfpr2 3626 mosn 3643 ralsnsg 3644 ralsns 3645 rexsns 3646 disjsn 3669 snprc 3672 euabsn2 3676 prmg 3728 snssOLD 3733 snssb 3740 difprsnss 3745 eqsnm 3770 snsssn 3776 snsspw 3779 dfnfc2 3842 uni0b 3849 uni0c 3850 sndisj 4014 unidif0 4185 exmid01 4216 rext 4233 exss 4245 frirrg 4368 ordsucim 4517 ordtriexmidlem 4536 ordtri2or2exmidlem 4543 onsucelsucexmidlem 4546 elirr 4558 sucprcreg 4566 fconstmpt 4691 opeliunxp 4699 restidsing 4981 dmsnopg 5118 dfmpt3 5357 nfunsn 5569 fsn 5709 fnasrn 5715 fnasrng 5717 fconstfvm 5755 eusvobj2 5883 opabex3d 6147 opabex3 6148 dcdifsnid 6530 ecexr 6565 ixp0x 6753 xpsnen 6848 fidifsnen 6899 difinfsn 7130 exmidonfinlem 7223 iccid 9957 fzsn 10098 fzpr 10109 fzdifsuc 10113 fsum2dlemstep 11477 prodsnf 11635 fprod1p 11642 fprodunsn 11647 fprod2dlemstep 11665 ef0lem 11703 1nprm 12149 mgmidsssn0 12863 mnd1id 12923 0subm 12951 trivsubgsnd 13157 kerf1ghm 13230 mulgrhm2 13925 restsn 14157 |
Copyright terms: Public domain | W3C validator |