Theorem rn0 5875

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 5869	. 2 ⊢ dom ∅ = ∅
2		dm0rn0 5873	. 2 ⊢ (dom ∅ = ∅ ↔ ran ∅ = ∅)
3	1, 2	mpbi 231	1 ⊢ ran ∅ = ∅

Syntax hints:   = wceq 1547  ∅c0 4268  dom cdm 5625  ran crn 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-cnv 5633  df-dm 5635  df-rn 5636

This theorem is referenced by:  ima0  6036  0ima  6037  rnxpid  6131  xpima  6140  f0  6715  rnfvprc  6828  2ndval  7941  frxp  8073  oarec  8494  fodomr  9063  fodomfir  9235  dfac5lem3  10045  itunitc  10341  relexprnd  15008  0rest  17390  arwval  18008  psgnsn  19493  oppglsm  19615  mpfrcl  22068  ply1frcl  22311  edgval  29143  0grsubgr  29372  0uhgrsubgr  29373  0ngrp  30607  bafval  30700  tocycf  33205  tocyc01  33206  domnprodeq0  33364  unitprodclb  33479  locfinref  34032  esumrnmpt2  34259  sibf0  34525  mvtval  35735  mrsubvrs  35757  mstaval  35779  mzpmfp  43203  dmnonrel  44041  imanonrel  44044  conrel1d  44114  clsneibex  44553  neicvgbex  44563  sge00  46826  dmrnxp  49334