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 3951 | . 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | df-rab 2921 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
3 | 2 | eqeq1i 2627 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅) |
4 | raln 2991 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑)) | |
5 | 1, 3, 4 | 3bitr4i 292 | 1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 ∧ wa 384 ∀wal 1481 = wceq 1483 ∈ wcel 1990 {cab 2608 ∀wral 2912 {crab 2916 ∅c0 3915 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rab 2921 df-v 3202 df-dif 3577 df-nul 3916 |
This theorem is referenced by: rabn0 3958 rabnc 3962 dffr2 5079 frc 5080 frirr 5091 wereu2 5111 tz6.26 5711 fndmdifeq0 6323 fnnfpeq0 6444 wemapso2 8458 wemapwe 8594 hashbclem 13236 hashbc 13237 smuval2 15204 smupvallem 15205 smu01lem 15207 smumullem 15214 phiprmpw 15481 hashgcdeq 15494 prmreclem4 15623 cshws0 15808 pmtrsn 17939 efgsfo 18152 00lsp 18981 dsmm0cl 20084 ordthauslem 21187 pthaus 21441 xkohaus 21456 hmeofval 21561 mumul 24907 musum 24917 ppiub 24929 lgsquadlem2 25106 umgrnloop0 26004 lfgrnloop 26020 numedglnl 26039 usgrnloop0ALT 26097 lfuhgr1v0e 26146 nbuhgr 26239 nbumgr 26243 uhgrnbgr0nb 26250 nbgr0vtxlem 26251 vtxd0nedgb 26384 vtxdusgr0edgnelALT 26392 1loopgrnb0 26398 usgrvd0nedg 26429 vtxdginducedm1lem4 26438 wwlks 26727 0enwwlksnge1 26749 wspn0 26820 rusgr0edg 26868 clwwlks 26879 clwwlksndisj 26973 vdn0conngrumgrv2 27056 eupth2lemb 27097 eulercrct 27102 frgrregorufr0 27188 numclwwlk3lem 27241 ofldchr 29814 measvuni 30277 dya2iocuni 30345 repr0 30689 reprlt 30697 reprgt 30699 subfacp1lem6 31167 poimirlem26 33435 poimirlem27 33436 cnambfre 33458 itg2addnclem2 33462 areacirclem5 33504 0dioph 37342 undisjrab 38505 supminfxr 39694 dvnprodlem3 40163 pimltmnf2 40911 pimconstlt0 40914 pimgtpnf2 40917 rmsupp0 42149 lcoc0 42211 |
Copyright terms: Public domain | W3C validator |