![]() |
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 5320 frc 5321 frirr 5332 wereu2 5352 tz6.26 5964 fndmdifeq0 6586 fnnfpeq0 6711 wemapso2 8747 wemapwe 8891 hashbclem 13550 hashbc 13551 wrdnfi 13637 smuval2 15610 smupvallem 15611 smu01lem 15613 smumullem 15620 phiprmpw 15885 hashgcdeq 15898 prmreclem4 16027 cshws0 16207 pmtrsn 18323 efgsfo 18537 00lsp 19376 dsmm0cl 20483 ordthauslem 21595 pthaus 21850 xkohaus 21865 hmeofval 21970 mumul 25359 musum 25369 ppiub 25381 lgsquadlem2 25558 umgrnloop0 26457 lfgrnloop 26473 numedglnl 26493 usgrnloop0ALT 26551 lfuhgr1v0e 26601 nbuhgr 26690 nbumgr 26694 uhgrnbgr0nb 26701 nbgr0vtxlem 26702 vtxd0nedgb 26836 vtxdusgr0edgnelALT 26844 1loopgrnb0 26850 usgrvd0nedg 26881 vtxdginducedm1lem4 26890 wwlks 27184 iswwlksnon 27202 iswspthsnon 27205 0enwwlksnge1 27213 wspn0 27304 rusgr0edg 27353 clwwlk 27363 clwwlkn 27415 clwwlkn0 27417 clwwlknon 27492 clwwlknon1nloop 27501 clwwlknondisj 27513 vdn0conngrumgrv2 27599 eupth2lemb 27641 eulercrct 27646 frgrregorufr0 27732 numclwwlk3lem2 27816 ofldchr 30376 measvuni 30875 dya2iocuni 30943 repr0 31291 reprlt 31299 reprgt 31301 subfacp1lem6 31766 frpomin 32327 frpomin2 32328 poimirlem26 34061 poimirlem27 34062 cnambfre 34083 itg2addnclem2 34087 areacirclem5 34129 0dioph 38302 undisjrab 39461 supminfxr 40599 dvnprodlem3 41091 pimltmnf2 41838 pimconstlt0 41841 pimgtpnf2 41844 rmsupp0 43164 lcoc0 43226 rrxsphere 43484 |
Copyright terms: Public domain | W3C validator |