![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elsn | GIF version |
Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
elsn | ⊢ (x ∈ {A} ↔ x = A) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-sn 3373 | . 2 ⊢ {A} = {x ∣ x = A} | |
2 | 1 | abeq2i 2145 | 1 ⊢ (x ∈ {A} ↔ x = A) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 98 = wceq 1242 ∈ wcel 1390 {csn 3367 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-4 1397 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-sb 1643 df-clab 2024 df-cleq 2030 df-clel 2033 df-sn 3373 |
This theorem is referenced by: dfpr2 3383 mosn 3398 ralsns 3399 rexsns 3400 rexsnsOLD 3401 disjsn 3423 snprc 3426 euabsn2 3430 prmg 3480 snss 3485 difprsnss 3493 eqsnm 3517 snsssn 3523 snsspw 3526 dfnfc2 3589 uni0b 3596 uni0c 3597 sndisj 3751 unidif0 3911 rext 3942 exss 3954 ordsucim 4192 ordtriexmidlem 4208 onsucelsucexmidlem 4214 elirr 4224 sucprcreg 4227 fconstmpt 4330 opeliunxp 4338 dmsnopg 4735 dfmpt3 4964 nfunsn 5150 fsn 5278 fnasrn 5284 fnasrng 5286 fconstfvm 5322 eusvobj2 5441 opabex3d 5690 opabex3 5691 ecexr 6047 xpsnen 6231 iccid 8564 fzsn 8699 fzpr 8709 fzdifsuc 8713 |
Copyright terms: Public domain | W3C validator |