Theorem rn0 5918

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 5912	. 2 ⊢ dom ∅ = ∅
2		dm0rn0 5916	. 2 ⊢ (dom ∅ = ∅ ↔ ran ∅ = ∅)
3	1, 2	mpbi 233	1 ⊢ ran ∅ = ∅

Syntax hints:   = wceq 1570  ∅c0 4287  dom cdm 5663  ran crn 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-cnv 5671  df-dm 5673  df-rn 5674

This theorem is referenced by:  ima0  6081  0ima  6082  rnxpid  6173  xpima  6182  f0  6761  rnfvprc  6877  2ndval  7990  frxp  8123  oarec  8548  fodomr  9117  fodomfir  9288  dfac5lem3  10110  itunitc  10406  relexprnd  15087  0rest  17483  arwval  18101  psgnsn  19591  oppglsm  19713  mpfrcl  22217  ply1frcl  22459  edgval  29377  0grsubgr  29606  0uhgrsubgr  29607  0ngrp  30841  bafval  30934  tocycf  33415  tocyc01  33416  domnprodeq0  33577  unitprodclb  33680  locfinref  34209  esumrnmpt2  34436  sibf0  34702  mvtval  35970  mrsubvrs  35992  mstaval  36014  mzpmfp  43458  dmnonrel  44296  imanonrel  44299  conrel1d  44369  clsneibex  44808  neicvgbex  44818  sge00  47070  dmrnxp  49592