![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rn0 | Structured version Visualization version Unicode version |
Description: The range of the empty set is empty. Part of Theorem 3.8(v) of [Monk1] p. 36. (Contributed by NM, 4-Jul-1994.) |
Ref | Expression |
---|---|
rn0 |
![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dm0 5048 |
. 2
![]() ![]() ![]() ![]() ![]() | |
2 | dm0rn0 5051 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbi 212 |
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 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pr 4639 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-rab 2746 df-v 3047 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-sn 3969 df-pr 3971 df-op 3975 df-br 4403 df-opab 4462 df-cnv 4842 df-dm 4844 df-rn 4845 |
This theorem is referenced by: ima0 5183 0ima 5184 rnxpid 5270 xpima 5279 f0 5764 2ndval 6796 frxp 6906 oarec 7263 fodomr 7723 dfac5lem3 8556 itunitc 8851 0rest 15328 arwval 15938 pmtrfrn 17099 psgnsn 17161 oppglsm 17294 mpfrcl 18741 ply1frcl 18907 nbgra0edg 25160 uvtx01vtx 25220 rusgra0edg 25683 0ngrp 25939 bafval 26223 locfinref 28668 esumrnmpt2 28889 sibf0 29167 mvtval 30138 mrsubrn 30151 mrsub0 30154 mrsubf 30155 mrsubccat 30156 mrsubcn 30157 mrsubco 30159 mrsubvrs 30160 elmsubrn 30166 msubrn 30167 msubf 30170 mstaval 30182 mzpmfp 35589 dmnonrel 36196 imanonrel 36199 conrel1d 36255 sge00 38218 0grsubgr 39350 0uhgrsubgr 39351 |
Copyright terms: Public domain | W3C validator |