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 4286. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) Avoid df-clel 2816, ax-8 2112. (Revised by Gino Giotto, 30-Aug-2024.) |
Ref | Expression |
---|---|
abn0 | ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ab0 4286 | . . 3 ⊢ ({𝑥 ∣ 𝜑} = ∅ ↔ ∀𝑥 ¬ 𝜑) | |
2 | 1 | notbii 323 | . 2 ⊢ (¬ {𝑥 ∣ 𝜑} = ∅ ↔ ¬ ∀𝑥 ¬ 𝜑) |
3 | df-ne 2940 | . 2 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ¬ {𝑥 ∣ 𝜑} = ∅) | |
4 | df-ex 1788 | . 2 ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) | |
5 | 2, 3, 4 | 3bitr4i 306 | 1 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 209 ∀wal 1541 = wceq 1543 ∃wex 1787 {cab 2714 ≠ wne 2939 ∅c0 4234 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-clab 2715 df-cleq 2729 df-ne 2940 df-dif 3866 df-nul 4235 |
This theorem is referenced by: intexab 5229 iinexg 5231 relimasn 5949 inisegn0 5963 mapprc 8509 modom 8876 tz9.1c 9343 scott0 9499 scott0s 9501 cp 9504 karden 9508 acnrcl 9653 aceq3lem 9731 cff 9859 cff1 9869 cfss 9876 domtriomlem 10053 axdclem 10130 nqpr 10625 supadd 11797 supmul 11801 hashf1lem2 14019 hashf1 14020 mreiincl 17096 efgval 19104 efger 19105 birthdaylem3 25833 disjex 30647 disjexc 30648 mppsval 33244 mblfinlem3 35551 ismblfin 35553 itg2addnc 35566 sdclem1 35636 upbdrech 42515 |
Copyright terms: Public domain | W3C validator |