Theorem rn0 5824

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 5818	. 2 ⊢ dom ∅ = ∅
2		dm0rn0 5823	. 2 ⊢ (dom ∅ = ∅ ↔ ran ∅ = ∅)
3	1, 2	mpbi 229	1 ⊢ ran ∅ = ∅

Syntax hints:   = wceq 1539  ∅c0 4253  dom cdm 5580  ran crn 5581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-cnv 5588  df-dm 5590  df-rn 5591

This theorem is referenced by:  ima0  5974  0ima  5975  rnxpid  6065  xpima  6074  f0  6639  rnfvprc  6750  2ndval  7807  frxp  7938  oarec  8355  fodomr  8864  dfac5lem3  9812  itunitc  10108  relexprnd  14687  0rest  17057  arwval  17674  psgnsn  19043  oppglsm  19162  mpfrcl  21205  ply1frcl  21394  edgval  27322  0grsubgr  27548  0uhgrsubgr  27549  0ngrp  28774  bafval  28867  tocycf  31286  tocyc01  31287  locfinref  31693  esumrnmpt2  31936  sibf0  32201  mvtval  33362  mrsubvrs  33384  mstaval  33406  mzpmfp  40485  dmnonrel  41087  imanonrel  41090  conrel1d  41160  clsneibex  41601  neicvgbex  41611  sge00  43804