![]() |
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 3606 | . 2 ⊢ (𝐴 ∈ {𝐵} → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)) | |
2 | 1 | ibi 176 | 1 ⊢ (𝐴 ∈ {𝐵} → 𝐴 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 ∈ wcel 2148 {csn 3591 |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2739 df-sn 3597 |
This theorem is referenced by: elsn2g 3624 nelsn 3626 disjsn2 3654 sssnm 3752 disjxsn 3998 pwntru 4196 opth1 4232 elsuci 4399 ordtri2orexmid 4518 onsucsssucexmid 4522 sosng 4695 elrelimasn 4989 ressn 5164 funcnvsn 5256 funinsn 5260 fvconst 5699 fmptap 5701 fmptapd 5702 fvunsng 5705 mposnif 5962 1stconst 6215 2ndconst 6216 reldmtpos 6247 tpostpos 6258 1domsn 6812 ac6sfi 6891 onunsnss 6909 snon0 6928 snexxph 6942 elfi2 6964 supsnti 6997 djuf1olem 7045 eldju2ndl 7064 eldju2ndr 7065 difinfsnlem 7091 pw1on 7218 elreal2 7807 ax1rid 7854 ltxrlt 8000 un0addcl 9185 un0mulcl 9186 elfzonlteqm1 10183 fxnn0nninf 10411 1exp 10522 hashinfuni 10728 hashennnuni 10730 hashprg 10759 zfz1isolemiso 10790 fisumss 11371 sumsnf 11388 fsumsplitsn 11389 fsum2dlemstep 11413 fisumcom2 11417 fprodssdc 11569 fprodunsn 11583 fprod2dlemstep 11601 fprodcom2fi 11605 fprodsplitsn 11612 divalgmod 11902 phi1 12189 dfphi2 12190 nnnn0modprm0 12225 exmidunben 12397 txdis1cn 13411 bj-nntrans 14325 bj-nnelirr 14327 pwtrufal 14369 sssneq 14374 exmidsbthrlem 14393 |
Copyright terms: Public domain | W3C validator |