![]() |
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 5927 | . 2 ⊢ dom ∅ = ∅ | |
2 | dm0rn0 5931 | . 2 ⊢ (dom ∅ = ∅ ↔ ran ∅ = ∅) | |
3 | 1, 2 | mpbi 229 | 1 ⊢ ran ∅ = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ∅c0 4325 dom cdm 5682 ran crn 5683 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5304 ax-nul 5311 ax-pr 5433 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-br 5154 df-opab 5216 df-cnv 5690 df-dm 5692 df-rn 5693 |
This theorem is referenced by: ima0 6086 0ima 6087 rnxpid 6184 xpima 6193 f0 6783 rnfvprc 6895 2ndval 8006 frxp 8140 oarec 8592 fodomr 9166 fodomfir 9370 dfac5lem3 10168 itunitc 10464 relexprnd 15053 0rest 17444 arwval 18065 psgnsn 19518 oppglsm 19640 mpfrcl 22100 ply1frcl 22309 edgval 28985 0grsubgr 29214 0uhgrsubgr 29215 0ngrp 30444 bafval 30537 tocycf 32995 tocyc01 32996 unitprodclb 33264 locfinref 33656 esumrnmpt2 33901 sibf0 34168 mvtval 35328 mrsubvrs 35350 mstaval 35372 mzpmfp 42404 dmnonrel 43257 imanonrel 43260 conrel1d 43330 clsneibex 43769 neicvgbex 43779 sge00 45997 |
Copyright terms: Public domain | W3C validator |