![]() |
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 4295 | . . 3 ⊢ ¬ 𝐵 ∈ ∅ | |
2 | eleq2 2827 | . . 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 1542 ∈ wcel 2107 ∅c0 4287 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-dif 3918 df-nul 4288 |
This theorem is referenced by: ne0i 4299 n0ii 4301 oprcl 4861 disjss3 5109 elfvdm 6884 mptrcl 6962 isomin 7287 ovrcl 7403 oalimcl 8512 omlimcl 8530 oaabs2 8600 ecexr 8660 elpmi 8791 elmapex 8793 pmresg 8815 pmsspw 8822 ixpssmap2g 8872 ixpssmapg 8873 resixpfo 8881 php3 9163 php3OLD 9175 cantnfp1lem2 9622 cantnflem1 9632 cnfcom2lem 9644 rankxplim2 9823 rankxplim3 9824 cardlim 9915 alephnbtwn 10014 ttukeylem5 10456 r1wunlim 10680 ssnn0fi 13897 ruclem13 16131 ramtub 16891 elbasfv 17096 elbasov 17097 restsspw 17320 homarcl 17921 grpidval 18523 odlem2 19328 efgrelexlema 19538 subcmn 19622 dvdsrval 20081 elocv 21088 pf1rcl 21731 matrcl 21775 0top 22349 ppttop 22373 pptbas 22374 restrcl 22524 ssrest 22543 iscnp2 22606 lmmo 22747 zfbas 23263 rnelfmlem 23319 isfcls 23376 isnghm 24103 iscau2 24657 itg2cnlem1 25142 itgsubstlem 25428 dchrrcl 26604 clwwlknnn 29019 0ringsubrg 32106 ssmxidllem 32278 eulerpartlemgvv 33016 indispconn 33868 cvmtop1 33894 cvmtop2 33895 mrsub0 34150 mrsubf 34151 mrsubccat 34152 mrsubcn 34153 mrsubco 34155 mrsubvrs 34156 msubf 34166 mclsrcl 34195 funpartlem 34556 tailfb 34878 nlpineqsn 35908 atbase 37780 llnbase 38001 lplnbase 38026 lvolbase 38070 osumcllem4N 38451 pexmidlem1N 38462 lhpbase 38490 mapco2g 41066 wepwsolem 41398 onov0suclim 41638 uneqsn 42371 ssfiunibd 43617 hoicvr 44863 0nelsetpreimafv 45656 |
Copyright terms: Public domain | W3C validator |