Theorem rn0 5907

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

Syntax hints:   = wceq 1563  ∅c0 4288  dom cdm 5652  ran crn 5653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-cnv 5660  df-dm 5662  df-rn 5663

This theorem is referenced by:  ima0  6070  0ima  6071  rnxpid  6163  xpima  6172  f0  6749  rnfvprc  6865  2ndval  7977  frxp  8110  oarec  8535  fodomr  9104  fodomfir  9275  dfac5lem3  10097  itunitc  10393  relexprnd  15075  0rest  17472  arwval  18090  psgnsn  19581  oppglsm  19703  mpfrcl  22196  ply1frcl  22439  edgval  29308  0grsubgr  29537  0uhgrsubgr  29538  0ngrp  30772  bafval  30865  tocycf  33350  tocyc01  33351  domnprodeq0  33512  unitprodclb  33618  locfinref  34148  esumrnmpt2  34375  sibf0  34641  mvtval  35863  mrsubvrs  35885  mstaval  35907  mzpmfp  43340  dmnonrel  44178  imanonrel  44181  conrel1d  44251  clsneibex  44690  neicvgbex  44700  sge00  46948  dmrnxp  49466