![]() |
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 3622 | . 2 ⊢ (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | |
2 | 1 | ibi 176 | 1 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1364 ∈ wcel 2160 {csn 3607 |
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 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 df-sn 3613 |
This theorem is referenced by: elsn2g 3640 nelsn 3642 disjsn2 3670 sssnm 3769 disjxsn 4016 pwntru 4217 opth1 4254 elsuci 4421 ordtri2orexmid 4540 onsucsssucexmid 4544 sosng 4717 elrelimasn 5012 ressn 5187 funcnvsn 5280 funinsn 5284 fvconst 5725 fmptap 5727 fmptapd 5728 fvunsng 5731 mposnif 5991 1stconst 6247 2ndconst 6248 reldmtpos 6279 tpostpos 6290 1domsn 6846 ac6sfi 6927 onunsnss 6946 snon0 6966 snexxph 6980 elfi2 7002 supsnti 7035 djuf1olem 7083 eldju2ndl 7102 eldju2ndr 7103 difinfsnlem 7129 pw1on 7256 elreal2 7860 ax1rid 7907 ltxrlt 8054 un0addcl 9240 un0mulcl 9241 elfzonlteqm1 10242 fxnn0nninf 10471 1exp 10583 hashinfuni 10792 hashennnuni 10794 hashprg 10823 zfz1isolemiso 10854 fisumss 11435 sumsnf 11452 fsumsplitsn 11453 fsum2dlemstep 11477 fisumcom2 11481 fprodssdc 11633 fprodunsn 11647 fprod2dlemstep 11665 fprodcom2fi 11669 fprodsplitsn 11676 divalgmod 11967 phi1 12254 dfphi2 12255 nnnn0modprm0 12290 exmidunben 12480 gsumress 12873 0nsg 13170 lsssn0 13703 lspsneq0 13759 txdis1cn 14255 bj-nntrans 15181 bj-nnelirr 15183 pwtrufal 15226 sssneq 15230 exmidsbthrlem 15249 |
Copyright terms: Public domain | W3C validator |