![]() |
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 4373. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) Avoid df-clel 2803, ax-8 2101. (Revised by GG, 30-Aug-2024.) |
Ref | Expression |
---|---|
abn0 | ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ab0 4373 | . . 3 ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑) | |
2 | 1 | notbii 319 | . 2 ⊢ (¬ {𝑥 ∣ 𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑) |
3 | df-ne 2931 | . 2 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ¬ {𝑥 ∣ 𝜑} = ∅) | |
4 | df-ex 1775 | . 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) | |
5 | 2, 3, 4 | 3bitr4i 302 | 1 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∀wal 1532 = wceq 1534 ∃wex 1774 {cab 2703 ≠ wne 2930 ∅c0 4323 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2704 df-cleq 2718 df-ne 2931 df-dif 3950 df-nul 4324 |
This theorem is referenced by: intexab 5337 iinexg 5339 relimasn 6085 inisegn0 6099 mapprc 8849 modom 9269 tz9.1c 9764 scott0 9920 scott0s 9922 cp 9925 karden 9929 acnrcl 10076 aceq3lem 10154 cff 10280 cff1 10290 cfss 10297 domtriomlem 10474 axdclem 10551 nqpr 11046 supadd 12226 supmul 12230 hashf1lem2 14468 hashf1 14469 mreiincl 17602 efgval 19709 efger 19710 birthdaylem3 26976 disjex 32510 disjexc 32511 mppsval 35411 mblfinlem3 37371 ismblfin 37373 itg2addnc 37386 sdclem1 37455 upbdrech 44954 |
Copyright terms: Public domain | W3C validator |