![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elsni | GIF version |
Description: There is only one element in a singleton. (Contributed by NM, 5-Jun-1994.) |
Ref | Expression |
---|---|
elsni | ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elsng 3489 | . 2 ⊢ (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | |
2 | 1 | ibi 175 | 1 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = 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: elsn2g 3505 disjsn2 3533 sssnm 3628 disjxsn 3873 opth1 4096 elsuci 4263 ordtri2orexmid 4376 onsucsssucexmid 4380 sosng 4550 ressn 5015 funcnvsn 5104 funinsn 5108 fvconst 5540 fmptap 5542 fmptapd 5543 fvunsng 5546 mposnif 5797 1stconst 6048 2ndconst 6049 reldmtpos 6080 tpostpos 6091 1domsn 6642 ac6sfi 6721 onunsnss 6734 snon0 6752 snexxph 6766 supsnti 6807 djuf1olem 6853 eldju2ndl 6872 eldju2ndr 6873 difinfsnlem 6899 elreal2 7518 ax1rid 7562 ltxrlt 7702 un0addcl 8862 un0mulcl 8863 elfzonlteqm1 9828 fxnn0nninf 10052 1exp 10163 hashinfuni 10364 hashennnuni 10366 hashprg 10395 zfz1isolemiso 10423 fisumss 11000 sumsnf 11017 fsumsplitsn 11018 fsum2dlemstep 11042 fisumcom2 11046 divalgmod 11419 phi1 11687 dfphi2 11688 exmidunben 11731 txdis1cn 12228 bj-nntrans 12734 bj-nnelirr 12736 pwtrufal 12777 pwntru 12778 exmidsbthrlem 12801 |
Copyright terms: Public domain | W3C validator |