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 3542 | . 2 ⊢ (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | |
2 | 1 | ibi 175 | 1 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1331 ∈ wcel 1480 {csn 3527 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-v 2688 df-sn 3533 |
This theorem is referenced by: elsn2g 3558 disjsn2 3586 sssnm 3681 disjxsn 3927 pwntru 4122 opth1 4158 elsuci 4325 ordtri2orexmid 4438 onsucsssucexmid 4442 sosng 4612 ressn 5079 funcnvsn 5168 funinsn 5172 fvconst 5608 fmptap 5610 fmptapd 5611 fvunsng 5614 mposnif 5865 1stconst 6118 2ndconst 6119 reldmtpos 6150 tpostpos 6161 1domsn 6713 ac6sfi 6792 onunsnss 6805 snon0 6824 snexxph 6838 elfi2 6860 supsnti 6892 djuf1olem 6938 eldju2ndl 6957 eldju2ndr 6958 difinfsnlem 6984 elreal2 7638 ax1rid 7685 ltxrlt 7830 un0addcl 9010 un0mulcl 9011 elfzonlteqm1 9987 fxnn0nninf 10211 1exp 10322 hashinfuni 10523 hashennnuni 10525 hashprg 10554 zfz1isolemiso 10582 fisumss 11161 sumsnf 11178 fsumsplitsn 11179 fsum2dlemstep 11203 fisumcom2 11207 divalgmod 11624 phi1 11895 dfphi2 11896 exmidunben 11939 txdis1cn 12447 bj-nntrans 13149 bj-nnelirr 13151 pwtrufal 13192 exmidsbthrlem 13217 |
Copyright terms: Public domain | W3C validator |