![]() |
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 4182 | . 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | df-rab 3099 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
3 | 2 | eqeq1i 2783 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅) |
4 | raln 3173 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑)) | |
5 | 1, 3, 4 | 3bitr4i 295 | 1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 198 ∧ wa 386 ∀wal 1599 = wceq 1601 ∈ wcel 2107 {cab 2763 ∀wral 3090 {crab 3094 ∅c0 4141 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rab 3099 df-dif 3795 df-nul 4142 |
This theorem is referenced by: rabn0 4188 rabnc 4190 dffr2 5322 frc 5323 frirr 5334 wereu2 5354 tz6.26 5966 fndmdifeq0 6588 fnnfpeq0 6713 wemapso2 8749 wemapwe 8893 hashbclem 13556 hashbc 13557 wrdnfi 13643 smuval2 15620 smupvallem 15621 smu01lem 15623 smumullem 15630 phiprmpw 15896 hashgcdeq 15909 prmreclem4 16038 cshws0 16218 pmtrsn 18334 efgsfo 18548 00lsp 19387 dsmm0cl 20494 ordthauslem 21606 pthaus 21861 xkohaus 21876 hmeofval 21981 mumul 25370 musum 25380 ppiub 25392 lgsquadlem2 25569 umgrnloop0 26474 lfgrnloop 26490 numedglnl 26510 usgrnloop0ALT 26568 lfuhgr1v0e 26618 nbuhgr 26707 nbumgr 26711 uhgrnbgr0nb 26718 nbgr0vtxlem 26719 vtxd0nedgb 26853 vtxdusgr0edgnelALT 26861 1loopgrnb0 26867 usgrvd0nedg 26898 vtxdginducedm1lem4 26907 wwlks 27201 iswwlksnon 27219 iswspthsnon 27222 0enwwlksnge1 27230 wspn0 27321 rusgr0edg 27370 clwwlk 27380 clwwlkn 27432 clwwlkn0 27434 clwwlknon 27509 clwwlknon1nloop 27518 clwwlknondisj 27530 vdn0conngrumgrv2 27616 eupth2lemb 27658 eulercrct 27663 frgrregorufr0 27749 numclwwlk3lem2 27833 ofldchr 30384 measvuni 30883 dya2iocuni 30951 repr0 31299 reprlt 31307 reprgt 31309 subfacp1lem6 31774 frpomin 32335 frpomin2 32336 poimirlem26 34070 poimirlem27 34071 cnambfre 34092 itg2addnclem2 34096 areacirclem5 34138 0dioph 38316 undisjrab 39475 supminfxr 40613 dvnprodlem3 41105 pimltmnf2 41852 pimconstlt0 41855 pimgtpnf2 41858 rmsupp0 43178 lcoc0 43240 rrxsphere 43498 |
Copyright terms: Public domain | W3C validator |