![]() |
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 4259. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) |
Ref | Expression |
---|---|
abn0 | ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfab1 2953 | . . 3 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑} | |
2 | 1 | n0f 4233 | . 2 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 𝑥 ∈ {𝑥 ∣ 𝜑}) |
3 | abid 2781 | . . 3 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) | |
4 | 3 | exbii 1833 | . 2 ⊢ (∃𝑥 𝑥 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥𝜑) |
5 | 2, 4 | bitri 276 | 1 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∃wex 1765 ∈ wcel 2083 {cab 2777 ≠ wne 2986 ∅c0 4217 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-ext 2771 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-dif 3868 df-nul 4218 |
This theorem is referenced by: intexab 5140 iinexg 5142 relimasn 5835 inisegn0 5844 mapprc 8267 modom 8572 tz9.1c 9025 scott0 9168 scott0s 9170 cp 9173 karden 9177 acnrcl 9321 aceq3lem 9399 cff 9523 cff1 9533 cfss 9540 domtriomlem 9717 axdclem 9794 nqpr 10289 supadd 11463 supmul 11467 hashf1lem2 13666 hashf1 13667 mreiincl 16700 efgval 18574 efger 18575 birthdaylem3 25217 disjex 30028 disjexc 30029 mppsval 32429 mblfinlem3 34483 ismblfin 34485 itg2addnc 34498 sdclem1 34571 upbdrech 41134 |
Copyright terms: Public domain | W3C validator |