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 2751 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | 1 | neq0f 3885 | 1 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 195 = wceq 1475 ∃wex 1695 ∈ wcel 1977 ∅c0 3874 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-dif 3543 df-nul 3875 |
This theorem is referenced by: ralidm 4027 snprc 4197 pwpw0 4284 sssn 4298 pwsnALT 4367 uni0b 4399 disjor 4567 isomin 6487 mpt2xneldm 7225 mpt2xopynvov0g 7227 mpt2xopxnop0 7228 erdisj 7681 ixpprc 7815 domunsn 7995 sucdom2 8041 isinf 8058 nfielex 8074 enp1i 8080 xpfi 8116 scottex 8631 acndom 8757 axcclem 9162 axpowndlem3 9300 canthp1lem1 9353 isumltss 14419 pf1rcl 19534 ppttop 20621 ntreq0 20691 txindis 21247 txcon 21302 fmfnfm 21572 ptcmplem2 21667 ptcmplem3 21668 bddmulibl 23411 wwlknndef 26265 wlk0 26289 clwwlknndef 26301 strlem1 28493 disjorf 28774 ddemeas 29626 bnj1143 30115 poimirlem25 32604 poimirlem27 32606 fnchoice 38211 founiiun0 38372 falseral0 40308 g01wlk0 40860 wwlksnndef 41111 clwwlksnndef 41198 nzerooringczr 41864 |
Copyright terms: Public domain | W3C validator |