Theorem rn0 5908

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

This proof depends on syntax axioms:   = wceq 1570  ∅c0 4279  dom cdm 5651  ran crn 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is used by:  ima0  6071  0ima  6072  rnxpid  6164  xpima  6173  f0  6755  rnfvprc  6871  2ndval  7993  frxp  8127  oarec  8554  fodomr  9131  fodomfir  9303  dfac5lem3  10185  itunitc  10480  relexprnd  15181  0rest  17580  arwval  18198  psgnsn  19714  oppglsm  19836  mpfrcl  22374  ply1frcl  22616  edgval  29609  0grsubgr  29841  0uhgrsubgr  29842  0ngrp  31095  bafval  31188  tocycf  33660  tocyc01  33661  domnprodeq0  33822  unitprodclb  33926  locfinref  34455  esumrnmpt2  34682  sibf0  34949  mvtval  36234  mrsubvrs  36256  mstaval  36278  mzpmfp  43711  dmnonrel  44549  imanonrel  44552  conrel1d  44622  clsneibex  45061  neicvgbex  45071  sge00  47330  dmrnxp  49891