![]() |
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 5571 | . 2 ⊢ dom ∅ = ∅ | |
2 | dm0rn0 5574 | . 2 ⊢ (dom ∅ = ∅ ↔ ran ∅ = ∅) | |
3 | 1, 2 | mpbi 222 | 1 ⊢ ran ∅ = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1656 ∅c0 4144 dom cdm 5342 ran crn 5343 |
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 5005 ax-nul 5013 ax-pr 5127 |
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 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 df-br 4874 df-opab 4936 df-cnv 5350 df-dm 5352 df-rn 5353 |
This theorem is referenced by: ima0 5722 0ima 5723 rnxpid 5808 xpima 5817 f0 6323 rnfvprc 6427 2ndval 7431 frxp 7551 oarec 7909 fodomr 8380 dfac5lem3 9261 itunitc 9558 0rest 16443 arwval 17045 psgnsn 18291 oppglsm 18408 mpfrcl 19878 ply1frcl 20043 edgval 26347 0grsubgr 26575 0uhgrsubgr 26576 0ngrp 27910 bafval 28003 locfinref 30442 esumrnmpt2 30664 sibf0 30930 mvtval 31932 mrsubvrs 31954 mstaval 31976 mzpmfp 38147 dmnonrel 38730 imanonrel 38733 conrel1d 38789 clsneibex 39233 neicvgbex 39243 sge00 41377 |
Copyright terms: Public domain | W3C validator |