| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > neq0 | Structured version Visualization version GIF version | ||
| Description: A class is not empty if and only if it has at least one element. Proposition 5.17(1) of [TakeutiZaring] p. 20. (Contributed by NM, 21-Jun-1993.) Avoid ax-11 2157, ax-12 2177. (Revised by GG, 28-Jun-2024.) |
| Ref | Expression |
|---|---|
| neq0 | ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ex 1780 | . . 3 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ ∀𝑥 ¬ 𝑥 ∈ 𝐴) | |
| 2 | eq0 4350 | . . 3 ⊢ (𝐴 = ∅ ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) | |
| 3 | 1, 2 | xchbinxr 335 | . 2 ⊢ (∃𝑥 𝑥 ∈ 𝐴 ↔ ¬ 𝐴 = ∅) |
| 4 | 3 | bicomi 224 | 1 ⊢ (¬ 𝐴 = ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 206 ∀wal 1538 = wceq 1540 ∃wex 1779 ∈ wcel 2108 ∅c0 4333 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-dif 3954 df-nul 4334 |
| This theorem is referenced by: n0 4353 falseral0 4516 snprc 4717 pwpw0 4813 sssn 4826 uni0b 4933 disjor 5125 rnep 5937 isomin 7357 mpoxneldm 8237 mpoxopynvov0g 8239 mpoxopxnop0 8240 erdisj 8799 ixpprc 8959 sucdom2OLD 9122 domunsn 9167 sucdom2 9243 isinf 9296 isinfOLD 9297 nfielex 9307 enp1iOLD 9314 xpfiOLD 9359 scottex 9925 acndom 10091 axcclem 10497 axpowndlem3 10639 canthp1lem1 10692 isumltss 15884 nzerooringczr 21491 pf1rcl 22353 ppttop 23014 ntreq0 23085 txindis 23642 txconn 23697 fmfnfm 23966 ptcmplem2 24061 ptcmplem3 24062 bddmulibl 25874 g0wlk0 29670 wwlksnndef 29925 strlem1 32269 disjorf 32592 ssdifidlprm 33486 1arithufdlem4 33575 ddemeas 34237 tgoldbachgt 34678 bnj1143 34804 prv1n 35436 pibt2 37418 poimirlem25 37652 poimirlem27 37654 ineleq 38355 eqvreldisj 38615 grucollcld 44279 relpmin 44973 fnchoice 45034 founiiun0 45195 mo0sn 48735 map0cor 48764 |
| Copyright terms: Public domain | W3C validator |