![]() |
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 4287 | . 2 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑)) | |
2 | df-rab 3115 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
3 | 2 | eqeq1i 2803 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = ∅) |
4 | raln 3123 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜑 ↔ ∀𝑥 ¬ (𝑥 ∈ 𝐴 ∧ 𝜑)) | |
5 | 1, 3, 4 | 3bitr4i 306 | 1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 209 ∧ wa 399 ∀wal 1536 = wceq 1538 ∈ wcel 2111 {cab 2776 ∀wral 3106 {crab 3110 ∅c0 4243 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rab 3115 df-dif 3884 df-nul 4244 |
This theorem is referenced by: rabn0 4293 rabnc 4295 dffr2 5484 frc 5485 frirr 5496 wereu2 5516 tz6.26 6147 fndmdifeq0 6791 fnnfpeq0 6917 wemapso2 9001 wemapwe 9144 hashbclem 13806 hashbc 13807 wrdnfi 13891 smuval2 15821 smupvallem 15822 smu01lem 15824 smumullem 15831 phiprmpw 16103 hashgcdeq 16116 prmreclem4 16245 cshws0 16427 pmtrsn 18639 efgsfo 18857 00lsp 19746 dsmm0cl 20429 ordthauslem 21988 pthaus 22243 xkohaus 22258 hmeofval 22363 mumul 25766 musum 25776 ppiub 25788 lgsquadlem2 25965 umgrnloop0 26902 lfgrnloop 26918 numedglnl 26937 usgrnloop0ALT 26995 lfuhgr1v0e 27044 nbuhgr 27133 nbumgr 27137 uhgrnbgr0nb 27144 nbgr0vtxlem 27145 vtxd0nedgb 27278 vtxdusgr0edgnelALT 27286 1loopgrnb0 27292 usgrvd0nedg 27323 vtxdginducedm1lem4 27332 wwlks 27621 iswwlksnon 27639 iswspthsnon 27642 0enwwlksnge1 27650 wspn0 27710 rusgr0edg 27759 clwwlk 27768 clwwlkn 27811 clwwlkn0 27813 clwwlknon 27875 clwwlknon1nloop 27884 clwwlknondisj 27896 vdn0conngrumgrv2 27981 eupth2lemb 28022 eulercrct 28027 frgrregorufr0 28109 numclwwlk3lem2 28169 ofldchr 30938 zarcls1 31222 measvuni 31583 dya2iocuni 31651 repr0 31992 reprlt 32000 reprgt 32002 nummin 32474 subfacp1lem6 32545 prv1n 32791 frpomin 33191 frpomin2 33192 poimirlem26 35083 poimirlem27 35084 cnambfre 35105 itg2addnclem2 35109 areacirclem5 35149 0dioph 39719 undisjrab 41010 supminfxr 42103 dvnprodlem3 42590 pimltmnf2 43336 pimconstlt0 43339 pimgtpnf2 43342 rmsupp0 44770 lcoc0 44831 rrxsphere 45162 |
Copyright terms: Public domain | W3C validator |