Theorem rn0 5875

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

Syntax hints:   = wceq 1541  ∅c0 4285  dom cdm 5624  ran crn 5625

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 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  ima0  6036  0ima  6037  rnxpid  6131  xpima  6140  f0  6715  rnfvprc  6828  2ndval  7936  frxp  8068  oarec  8489  fodomr  9056  fodomfir  9228  dfac5lem3  10035  itunitc  10331  relexprnd  14971  0rest  17349  arwval  17967  psgnsn  19449  oppglsm  19571  mpfrcl  22040  ply1frcl  22262  edgval  29122  0grsubgr  29351  0uhgrsubgr  29352  0ngrp  30586  bafval  30679  tocycf  33199  tocyc01  33200  domnprodeq0  33358  unitprodclb  33470  locfinref  33998  esumrnmpt2  34225  sibf0  34491  mvtval  35694  mrsubvrs  35716  mstaval  35738  mzpmfp  42985  dmnonrel  43827  imanonrel  43830  conrel1d  43900  clsneibex  44339  neicvgbex  44349  sge00  46616  dmrnxp  49078