| 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 4380. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) Avoid df-clel 2816, ax-8 2110. (Revised by GG, 30-Aug-2024.) |
| Ref | Expression |
|---|---|
| abn0 | ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ab0 4380 | . . 3 ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑) | |
| 2 | 1 | notbii 320 | . 2 ⊢ (¬ {𝑥 ∣ 𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑) |
| 3 | df-ne 2941 | . 2 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ¬ {𝑥 ∣ 𝜑} = ∅) | |
| 4 | df-ex 1780 | . 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) | |
| 5 | 2, 3, 4 | 3bitr4i 303 | 1 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ↔ wb 206 ∀wal 1538 = wceq 1540 ∃wex 1779 {cab 2714 ≠ wne 2940 ∅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-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-ne 2941 df-dif 3954 df-nul 4334 |
| This theorem is referenced by: intexab 5346 iinexg 5348 relimasn 6103 inisegn0 6116 mapprc 8870 modom 9280 tz9.1c 9770 scott0 9926 scott0s 9928 cp 9931 karden 9935 acnrcl 10082 aceq3lem 10160 cff 10288 cff1 10298 cfss 10305 domtriomlem 10482 axdclem 10559 nqpr 11054 supadd 12236 supmul 12240 hashf1lem2 14495 hashf1 14496 mreiincl 17639 efgval 19735 efger 19736 birthdaylem3 26996 disjex 32605 disjexc 32606 mppsval 35577 mblfinlem3 37666 ismblfin 37668 itg2addnc 37681 sdclem1 37750 upbdrech 45317 |
| Copyright terms: Public domain | W3C validator |