| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > n0i | Structured version Visualization version GIF version | ||
| Description: If a class has elements, then it is not empty. (Contributed by NM, 31-Dec-1993.) |
| Ref | Expression |
|---|---|
| n0i | ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | noel 4338 | . . 3 ⊢ ¬ 𝐵 ∈ ∅ | |
| 2 | eleq2 2830 | . . 3 ⊢ (𝐴 = ∅ → (𝐵 ∈ 𝐴 ↔ 𝐵 ∈ ∅)) | |
| 3 | 1, 2 | mtbiri 327 | . 2 ⊢ (𝐴 = ∅ → ¬ 𝐵 ∈ 𝐴) |
| 4 | 3 | con2i 139 | 1 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1540 ∈ wcel 2108 ∅c0 4333 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-dif 3954 df-nul 4334 |
| This theorem is referenced by: ne0i 4341 n0ii 4343 oprcl 4899 disjss3 5142 elfvdm 6943 mptrcl 7025 isomin 7357 ovrcl 7472 elfvov1 7473 elfvov2 7474 oalimcl 8598 omlimcl 8616 nnaordex2 8677 oaabs2 8687 ecexr 8750 elpmi 8886 elmapex 8888 pmresg 8910 pmsspw 8917 ixpssmap2g 8967 ixpssmapg 8968 resixpfo 8976 php3 9249 php3OLD 9261 cantnfp1lem2 9719 cantnflem1 9729 cnfcom2lem 9741 rankxplim2 9920 rankxplim3 9921 cardlim 10012 alephnbtwn 10111 ttukeylem5 10553 r1wunlim 10777 ssnn0fi 14026 ruclem13 16278 ramtub 17050 elbasfv 17253 elbasov 17254 restsspw 17476 homarcl 18073 grpidval 18674 odlem2 19557 efgrelexlema 19767 subcmn 19855 dvdsrval 20361 elocv 21686 pf1rcl 22353 matrcl 22416 0top 22990 ppttop 23014 pptbas 23015 restrcl 23165 ssrest 23184 iscnp2 23247 lmmo 23388 zfbas 23904 rnelfmlem 23960 isfcls 24017 isnghm 24744 iscau2 25311 itg2cnlem1 25796 itgsubstlem 26089 dchrrcl 27284 clwwlknnn 30052 0ringsubrg 33255 ssdifidllem 33484 ssmxidllem 33501 eulerpartlemgvv 34378 indispconn 35239 cvmtop1 35265 cvmtop2 35266 mrsub0 35521 mrsubf 35522 mrsubccat 35523 mrsubcn 35524 mrsubco 35526 mrsubvrs 35527 msubf 35537 mclsrcl 35566 funpartlem 35943 tailfb 36378 nlpineqsn 37409 atbase 39290 llnbase 39511 lplnbase 39536 lvolbase 39580 osumcllem4N 39961 pexmidlem1N 39972 lhpbase 40000 mapco2g 42725 wepwsolem 43054 onov0suclim 43287 uneqsn 44038 relpmin 44973 ssfiunibd 45321 hoicvr 46563 0nelsetpreimafv 47377 termchomn0 49129 |
| Copyright terms: Public domain | W3C validator |