![]() |
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 4098. (Contributed by NM, 26-Dec-1996.) (Proof shortened by Mario Carneiro, 11-Nov-2016.) |
Ref | Expression |
---|---|
abn0 | ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfab1 2915 | . . 3 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑} | |
2 | 1 | n0f 4075 | . 2 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 𝑥 ∈ {𝑥 ∣ 𝜑}) |
3 | abid 2759 | . . 3 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) | |
4 | 3 | exbii 1924 | . 2 ⊢ (∃𝑥 𝑥 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑥𝜑) |
5 | 2, 4 | bitri 264 | 1 ⊢ ({𝑥 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∃wex 1852 ∈ wcel 2145 {cab 2757 ≠ wne 2943 ∅c0 4063 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 835 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-v 3353 df-dif 3726 df-nul 4064 |
This theorem is referenced by: intexab 4953 iinexg 4955 relimasn 5629 inisegn0 5638 mapprc 8013 modom 8317 tz9.1c 8770 scott0 8913 scott0s 8915 cp 8918 karden 8922 acnrcl 9065 aceq3lem 9143 cff 9272 cff1 9282 cfss 9289 domtriomlem 9466 axdclem 9543 nqpr 10038 supadd 11193 supmul 11197 hashf1lem2 13442 hashf1 13443 mreiincl 16464 efgval 18337 efger 18338 birthdaylem3 24901 disjex 29743 disjexc 29744 mppsval 31807 mblfinlem3 33781 ismblfin 33783 itg2addnc 33796 sdclem1 33871 upbdrech 40036 |
Copyright terms: Public domain | W3C validator |