![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ne0i | GIF version |
Description: If a set has elements, it is not empty. A set with elements is also inhabited, see elex2 2649. (Contributed by NM, 31-Dec-1993.) |
Ref | Expression |
---|---|
ne0i | ⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | n0i 3307 | . 2 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅) | |
2 | 1 | neneqad 2341 | 1 ⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1445 ≠ wne 2262 ∅c0 3302 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 582 ax-in2 583 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ne 2263 df-v 2635 df-dif 3015 df-nul 3303 |
This theorem is referenced by: ne0d 3309 ne0ii 3311 vn0 3312 inelcm 3362 rzal 3399 rexn0 3400 snnzg 3579 prnz 3584 tpnz 3587 onn0 4251 nn0eln0 4461 ordge1n0im 6238 nnmord 6316 map0g 6485 phpm 6661 fiintim 6719 addclpi 6983 mulclpi 6984 uzn0 9133 iccsupr 9532 |
Copyright terms: Public domain | W3C validator |