| 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 3648 | . 2 ⊢ (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | |
| 2 | 1 | ibi 176 | 1 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 = wceq 1373 ∈ wcel 2176 {csn 3633 |
| 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 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-ext 2187 |
| This theorem depends on definitions: df-bi 117 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-v 2774 df-sn 3639 |
| This theorem is referenced by: elsn2g 3666 nelsn 3668 disjsn2 3696 sssnm 3795 disjxsn 4042 pwntru 4243 opth1 4280 elsuci 4450 ordtri2orexmid 4571 onsucsssucexmid 4575 sosng 4748 elrelimasn 5048 ressn 5223 funcnvsn 5319 funinsn 5323 funopdmsn 5764 fvconst 5772 fmptap 5774 fmptapd 5775 fvunsng 5778 mposnif 6039 1stconst 6307 2ndconst 6308 reldmtpos 6339 tpostpos 6350 1domsn 6914 ac6sfi 6995 onunsnss 7014 snon0 7037 snexxph 7052 elfi2 7074 supsnti 7107 djuf1olem 7155 eldju2ndl 7174 eldju2ndr 7175 difinfsnlem 7201 pw1on 7338 elreal2 7943 ax1rid 7990 ltxrlt 8138 un0addcl 9328 un0mulcl 9329 elfzonlteqm1 10339 xnn0nnen 10582 fxnn0nninf 10584 seqf1og 10666 1exp 10713 hashinfuni 10922 hashennnuni 10924 hashprg 10953 zfz1isolemiso 10984 fisumss 11703 sumsnf 11720 fsumsplitsn 11721 fsum2dlemstep 11745 fisumcom2 11749 fprodssdc 11901 fprodunsn 11915 fprod2dlemstep 11933 fprodcom2fi 11937 fprodsplitsn 11944 divalgmod 12238 phi1 12541 dfphi2 12542 nnnn0modprm0 12578 exmidunben 12797 gsumress 13227 0nsg 13550 gsumfzsnfd 13681 lsssn0 14132 lspsneq0 14188 txdis1cn 14750 plyaddlem1 15219 plymullem1 15220 plycoeid3 15229 plycj 15233 bj-nntrans 15887 bj-nnelirr 15889 pwtrufal 15934 sssneq 15939 exmidsbthrlem 15961 |
| Copyright terms: Public domain | W3C validator |