![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > abn0 | Structured version Visualization version GIF version |
Description: Nonempty class abstraction. See also ab0 4334. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) Avoid df-clel 2814, ax-8 2108. (Revised by Gino Giotto, 30-Aug-2024.) |
Ref | Expression |
---|---|
abn0 | ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ab0 4334 | . . 3 ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑) | |
2 | 1 | notbii 319 | . 2 ⊢ (¬ {𝑥 ∣ 𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑) |
3 | df-ne 2944 | . 2 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ¬ {𝑥 ∣ 𝜑} = ∅) | |
4 | df-ex 1782 | . 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) | |
5 | 2, 3, 4 | 3bitr4i 302 | 1 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∀wal 1539 = wceq 1541 ∃wex 1781 {cab 2713 ≠ wne 2943 ∅c0 4282 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2714 df-cleq 2728 df-ne 2944 df-dif 3913 df-nul 4283 |
This theorem is referenced by: intexab 5296 iinexg 5298 relimasn 6036 inisegn0 6050 mapprc 8769 modom 9188 tz9.1c 9666 scott0 9822 scott0s 9824 cp 9827 karden 9831 acnrcl 9978 aceq3lem 10056 cff 10184 cff1 10194 cfss 10201 domtriomlem 10378 axdclem 10455 nqpr 10950 supadd 12123 supmul 12127 hashf1lem2 14355 hashf1 14356 mreiincl 17476 efgval 19499 efger 19500 birthdaylem3 26303 disjex 31510 disjexc 31511 mppsval 34166 mblfinlem3 36117 ismblfin 36119 itg2addnc 36132 sdclem1 36202 upbdrech 43529 |
Copyright terms: Public domain | W3C validator |