Theorem rn0 5921

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

This proof depends on syntax axioms:   = wceq 1570  ∅c0 4289  dom cdm 5666  ran crn 5667

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

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 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-cnv 5674  df-dm 5676  df-rn 5677

This theorem is used by:  ima0  6084  0ima  6085  rnxpid  6176  xpima  6185  f0  6766  rnfvprc  6882  2ndval  7998  frxp  8131  oarec  8556  fodomr  9126  fodomfir  9297  dfac5lem3  10128  itunitc  10423  relexprnd  15111  0rest  17507  arwval  18125  psgnsn  19621  oppglsm  19743  mpfrcl  22273  ply1frcl  22515  edgval  29436  0grsubgr  29665  0uhgrsubgr  29666  0ngrp  30900  bafval  30993  tocycf  33468  tocyc01  33469  domnprodeq0  33630  unitprodclb  33733  locfinref  34262  esumrnmpt2  34489  sibf0  34755  mvtval  36012  mrsubvrs  36034  mstaval  36056  mzpmfp  43518  dmnonrel  44356  imanonrel  44359  conrel1d  44429  clsneibex  44868  neicvgbex  44878  sge00  47130  dmrnxp  49655