![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > neq0 | Structured version Visualization version GIF version |
Description: A nonempty class has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
neq0 | ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2902 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | 1 | neq0f 4069 | 1 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 = wceq 1632 ∃wex 1853 ∈ wcel 2139 ∅c0 4058 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-v 3342 df-dif 3718 df-nul 4059 |
This theorem is referenced by: ralidm 4219 falseral0 4225 snprc 4397 pwpw0 4489 sssn 4503 pwsnALT 4581 uni0b 4615 disjor 4786 isomin 6750 mpt2xneldm 7507 mpt2xopynvov0g 7509 mpt2xopxnop0 7510 erdisj 7961 ixpprc 8095 domunsn 8275 sucdom2 8321 isinf 8338 nfielex 8354 enp1i 8360 xpfi 8396 scottex 8921 acndom 9064 axcclem 9471 axpowndlem3 9613 canthp1lem1 9666 isumltss 14779 pf1rcl 19915 ppttop 21013 ntreq0 21083 txindis 21639 txconn 21694 fmfnfm 21963 ptcmplem2 22058 ptcmplem3 22059 bddmulibl 23804 g0wlk0 26758 wwlksnndef 27023 strlem1 29418 disjorf 29699 ddemeas 30608 tgoldbachgt 31050 bnj1143 31168 poimirlem25 33747 poimirlem27 33749 ineleq 34442 fnchoice 39687 founiiun0 39876 nzerooringczr 42582 |
Copyright terms: Public domain | W3C validator |