![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rabeq0 | Structured version Visualization version Unicode version |
Description: Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010.) |
Ref | Expression |
---|---|
rabeq0 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralnex 2833 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | rabn0 3751 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | necon1bbii 2672 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | bitr2i 254 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-ral 2741 df-rex 2742 df-rab 2745 df-v 3046 df-dif 3406 df-nul 3731 |
This theorem is referenced by: rabnc 3755 dffr2 4798 frc 4799 frirr 4810 wereu2 4830 tz6.26 5410 fndmdifeq0 5986 fnnfpeq0 6093 wemapso2 8065 wemapwe 8199 hashbclem 12612 hashbc 12613 smuval2 14449 smupvallem 14450 smu01lem 14452 smumullem 14459 phiprmpw 14717 prmreclem4 14856 cshws0 15065 pmtrsn 17153 efgsfo 17382 00lsp 18197 dsmm0cl 19296 ordthauslem 20392 pthaus 20646 xkohaus 20661 hmeofval 20766 mumul 24101 musum 24113 ppiub 24125 lgsquadlem2 24276 usgranloop0 25100 usgra1v 25110 nbusgra 25149 nbgra0nb 25150 nbgra0edg 25153 cusgrasizeindslem2 25195 uvtx0 25212 clwwlkn0 25495 vdgr1b 25625 vdgr1a 25627 vdusgra0nedg 25629 usgravd0nedg 25639 eupath2 25701 vdn0frgrav2 25744 vdgn0frgrav2 25745 frgraregorufr0 25773 2spot0 25785 numclwwlkdisj 25801 numclwwlk3lem 25829 ofldchr 28570 measvuni 29029 dya2iocuni 29098 subfacp1lem6 29901 poimirlem26 31959 poimirlem27 31960 cnambfre 31982 itg2addnclem2 31987 areacirclem5 32029 0dioph 35615 hashgcdeq 36069 undisjrab 36648 dvnprodlem3 37817 umgrnloop0 39183 usgrnloop0ALT 39274 usgr1vr 39312 nbuhgr 39394 nbumgr 39398 uhgrnbgr0nb 39405 nbgr0vtxlem 39406 uhgrvd0nedgb 39528 vtxdusgr0edgnelALT 39533 uspgrloopnb0 39539 usgrvd0nedg 39553 rmsupp0 40140 lcoc0 40202 |
Copyright terms: Public domain | W3C validator |