Theorem rn0 5870

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.)

Assertion

Ref	Expression
rn0	⊢ ran ∅ = ∅

Proof of Theorem rn0

Step	Hyp	Ref	Expression
1		dm0 5864	. 2 ⊢ dom ∅ = ∅
2		dm0rn0 5868	. 2 ⊢ (dom ∅ = ∅ ↔ ran ∅ = ∅)
3	1, 2	mpbi 230	1 ⊢ ran ∅ = ∅

Syntax hints:   = wceq 1541  ∅c0 4282  dom cdm 5619  ran crn 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-cnv 5627  df-dm 5629  df-rn 5630

This theorem is referenced by:  ima0  6030  0ima  6031  rnxpid  6125  xpima  6134  f0  6709  rnfvprc  6822  2ndval  7930  frxp  8062  oarec  8483  fodomr  9048  fodomfir  9219  dfac5lem3  10023  itunitc  10319  relexprnd  14957  0rest  17335  arwval  17952  psgnsn  19434  oppglsm  19556  mpfrcl  22021  ply1frcl  22234  edgval  29029  0grsubgr  29258  0uhgrsubgr  29259  0ngrp  30493  bafval  30586  tocycf  33093  tocyc01  33094  unitprodclb  33361  locfinref  33875  esumrnmpt2  34102  sibf0  34368  mvtval  35565  mrsubvrs  35587  mstaval  35609  mzpmfp  42864  dmnonrel  43707  imanonrel  43710  conrel1d  43780  clsneibex  44219  neicvgbex  44229  sge00  46498  dmrnxp  48961