Theorem rn0 5923

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 5918	. 2 ⊢ dom ∅ = ∅
2		dm0rn0 5922	. 2 ⊢ (dom ∅ = ∅ ↔ ran ∅ = ∅)
3	1, 2	mpbi 229	1 ⊢ ran ∅ = ∅

Syntax hints:   = wceq 1541  ∅c0 4321  dom cdm 5675  ran crn 5676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-cnv 5683  df-dm 5685  df-rn 5686

This theorem is referenced by:  ima0  6073  0ima  6074  rnxpid  6169  xpima  6178  f0  6769  rnfvprc  6882  2ndval  7974  frxp  8108  oarec  8558  fodomr  9124  dfac5lem3  10116  itunitc  10412  relexprnd  14991  0rest  17371  arwval  17989  psgnsn  19382  oppglsm  19504  mpfrcl  21639  ply1frcl  21828  edgval  28298  0grsubgr  28524  0uhgrsubgr  28525  0ngrp  29751  bafval  29844  tocycf  32263  tocyc01  32264  locfinref  32809  esumrnmpt2  33054  sibf0  33321  mvtval  34479  mrsubvrs  34501  mstaval  34523  mzpmfp  41470  dmnonrel  42326  imanonrel  42329  conrel1d  42399  clsneibex  42838  neicvgbex  42848  sge00  45078