![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rn0 | Structured version Visualization version GIF 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 | ⊢ ran ∅ = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dm0 5575 | . 2 ⊢ dom ∅ = ∅ | |
2 | dm0rn0 5578 | . 2 ⊢ (dom ∅ = ∅ ↔ ran ∅ = ∅) | |
3 | 1, 2 | mpbi 222 | 1 ⊢ ran ∅ = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1656 ∅c0 4146 dom cdm 5346 ran crn 5347 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 ax-sep 5007 ax-nul 5015 ax-pr 5129 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-mo 2605 df-eu 2640 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4147 df-if 4309 df-sn 4400 df-pr 4402 df-op 4406 df-br 4876 df-opab 4938 df-cnv 5354 df-dm 5356 df-rn 5357 |
This theorem is referenced by: ima0 5726 0ima 5727 rnxpid 5812 xpima 5821 f0 6327 rnfvprc 6431 2ndval 7436 frxp 7556 oarec 7914 fodomr 8386 dfac5lem3 9268 itunitc 9565 0rest 16450 arwval 17052 psgnsn 18298 oppglsm 18415 mpfrcl 19885 ply1frcl 20050 edgval 26354 0grsubgr 26582 0uhgrsubgr 26583 0ngrp 27917 bafval 28010 locfinref 30449 esumrnmpt2 30671 sibf0 30937 mvtval 31939 mrsubvrs 31961 mstaval 31983 mzpmfp 38153 dmnonrel 38736 imanonrel 38739 conrel1d 38795 clsneibex 39239 neicvgbex 39249 sge00 41382 |
Copyright terms: Public domain | W3C validator |