![]() |
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 2605 | . 2 ⊢ 𝑥 ∈ V | |
2 | 1 | elsn 3422 | 1 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 103 = wceq 1285 ∈ wcel 1434 {csn 3406 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1687 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-v 2604 df-sn 3412 |
This theorem is referenced by: dfpr2 3425 mosn 3437 ralsnsg 3438 ralsns 3439 rexsns 3440 disjsn 3462 snprc 3465 euabsn2 3469 prmg 3519 snss 3524 difprsnss 3532 eqsnm 3555 snsssn 3561 snsspw 3564 dfnfc2 3627 uni0b 3634 uni0c 3635 sndisj 3789 unidif0 3949 rext 3978 exss 3990 frirrg 4113 ordsucim 4252 ordtriexmidlem 4271 ordtri2or2exmidlem 4277 onsucelsucexmidlem 4280 elirr 4292 sucprcreg 4300 fconstmpt 4413 opeliunxp 4421 dmsnopg 4822 dfmpt3 5052 nfunsn 5239 fsn 5367 fnasrn 5373 fnasrng 5375 fconstfvm 5411 eusvobj2 5529 opabex3d 5779 opabex3 5780 nndifsnid 6146 ecexr 6177 xpsnen 6365 fidifsnen 6405 fidifsnid 6406 iccid 9024 fzsn 9160 fzpr 9170 fzdifsuc 9174 1nprm 10640 |
Copyright terms: Public domain | W3C validator |