Theorem rn0 5939

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 5934	. 2 ⊢ dom ∅ = ∅
2		dm0rn0 5938	. 2 ⊢ (dom ∅ = ∅ ↔ ran ∅ = ∅)
3	1, 2	mpbi 230	1 ⊢ ran ∅ = ∅

Syntax hints:   = wceq 1537  ∅c0 4339  dom cdm 5689  ran crn 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-cnv 5697  df-dm 5699  df-rn 5700

This theorem is referenced by:  ima0  6097  0ima  6098  rnxpid  6195  xpima  6204  f0  6790  rnfvprc  6901  2ndval  8016  frxp  8150  oarec  8599  fodomr  9167  fodomfir  9366  dfac5lem3  10163  itunitc  10459  relexprnd  15084  0rest  17476  arwval  18097  psgnsn  19553  oppglsm  19675  mpfrcl  22127  ply1frcl  22338  edgval  29081  0grsubgr  29310  0uhgrsubgr  29311  0ngrp  30540  bafval  30633  tocycf  33120  tocyc01  33121  unitprodclb  33397  locfinref  33802  esumrnmpt2  34049  sibf0  34316  mvtval  35485  mrsubvrs  35507  mstaval  35529  mzpmfp  42735  dmnonrel  43580  imanonrel  43583  conrel1d  43653  clsneibex  44092  neicvgbex  44102  sge00  46332