Theorem rn0 5610

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 5571	. 2 ⊢ dom ∅ = ∅
2		dm0rn0 5574	. 2 ⊢ (dom ∅ = ∅ ↔ ran ∅ = ∅)
3	1, 2	mpbi 222	1 ⊢ ran ∅ = ∅

Syntax hints:   = wceq 1656  ∅c0 4144  dom cdm 5342  ran crn 5343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pr 5127

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-br 4874  df-opab 4936  df-cnv 5350  df-dm 5352  df-rn 5353

This theorem is referenced by:  ima0  5722  0ima  5723  rnxpid  5808  xpima  5817  f0  6323  rnfvprc  6427  2ndval  7431  frxp  7551  oarec  7909  fodomr  8380  dfac5lem3  9261  itunitc  9558  0rest  16443  arwval  17045  psgnsn  18291  oppglsm  18408  mpfrcl  19878  ply1frcl  20043  edgval  26347  0grsubgr  26575  0uhgrsubgr  26576  0ngrp  27910  bafval  28003  locfinref  30442  esumrnmpt2  30664  sibf0  30930  mvtval  31932  mrsubvrs  31954  mstaval  31976  mzpmfp  38147  dmnonrel  38730  imanonrel  38733  conrel1d  38789  clsneibex  39233  neicvgbex  39243  sge00  41377