![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rabeq0 | Structured version Visualization version GIF version |
Description: Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.) (Revised by BJ, 16-Jul-2021.) |
Ref | Expression |
---|---|
rabeq0 | ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ab0 4375 | . 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | df-rab 3430 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
3 | 2 | eqeq1i 2733 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅) |
4 | raln 3066 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑)) | |
5 | 1, 3, 4 | 3bitr4i 303 | 1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 395 ∀wal 1532 = wceq 1534 ∈ wcel 2099 {cab 2705 ∀wral 3058 {crab 3429 ∅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 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2706 df-cleq 2720 df-ral 3059 df-rab 3430 df-dif 3950 df-nul 4324 |
This theorem is referenced by: rabn0 4386 rabnc 4388 dffr2ALT 5643 wereu2 5675 frpomin 6346 frpomin2 6347 tz6.26OLD 6354 fndmdifeq0 7053 fnnfpeq0 7187 wemapso2 9577 wemapwe 9721 hashbclem 14444 hashbc 14445 wrdnfi 14531 smuval2 16457 smupvallem 16458 smu01lem 16460 smumullem 16467 phiprmpw 16745 hashgcdeq 16758 prmreclem4 16888 cshws0 17071 pmtrsn 19474 efgsfo 19694 00lsp 20865 dsmm0cl 21674 ordthauslem 23300 pthaus 23555 xkohaus 23570 hmeofval 23675 mumul 27126 musum 27136 ppiub 27150 lgsquadlem2 27327 umgrnloop0 28935 lfgrnloop 28951 numedglnl 28970 usgrnloop0ALT 29031 lfuhgr1v0e 29080 nbuhgr 29169 nbumgr 29173 uhgrnbgr0nb 29180 nbgr0vtxlem 29181 vtxd0nedgb 29315 vtxdusgr0edgnelALT 29323 1loopgrnb0 29329 usgrvd0nedg 29360 vtxdginducedm1lem4 29369 wwlks 29659 iswwlksnon 29677 iswspthsnon 29680 0enwwlksnge1 29688 wspn0 29748 rusgr0edg 29797 clwwlk 29806 clwwlkn 29849 clwwlkn0 29851 clwwlknon 29913 clwwlknon1nloop 29922 clwwlknondisj 29934 vdn0conngrumgrv2 30019 eupth2lemb 30060 eulercrct 30065 frgrregorufr0 30147 numclwwlk3lem2 30207 ofldchr 33042 zarcls1 33470 measvuni 33833 dya2iocuni 33903 repr0 34243 reprlt 34251 reprgt 34253 nummin 34714 subfacp1lem6 34795 prv1n 35041 poimirlem26 37119 poimirlem27 37120 cnambfre 37141 itg2addnclem2 37145 areacirclem5 37185 sticksstones1 41618 nna4b4nsq 42084 0dioph 42198 undisjrab 43743 supminfxr 44846 dvnprodlem3 45336 pimltmnf2f 46085 pimconstlt0 46089 pimgtpnf2f 46093 rmsupp0 47432 lcoc0 47490 rrxsphere 47821 |
Copyright terms: Public domain | W3C validator |