![]() |
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 2626. (Contributed by NM, 31-Dec-1993.) |
Ref | Expression |
---|---|
ne0i | ⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | n0i 3274 | . 2 ⊢ (𝐵 ∈ 𝐴 → ¬ 𝐴 = ∅) | |
2 | 1 | neneqad 2328 | 1 ⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1434 ≠ wne 2249 ∅c0 3269 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ne 2250 df-v 2614 df-dif 2986 df-nul 3270 |
This theorem is referenced by: vn0 3276 inelcm 3325 rzal 3360 rexn0 3361 snnzg 3531 prnz 3536 tpnz 3539 onn0 4190 nn0eln0 4395 ordge1n0im 6130 nnmord 6204 map0g 6373 phpm 6509 addclpi 6787 mulclpi 6788 uzn0 8927 iccsupr 9277 |
Copyright terms: Public domain | W3C validator |