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 ∅ = ∅

This proof depends on syntax axioms:   = wceq 1569  ∅c0 4278  dom cdm 5650  ran crn 5651

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-cnv 5658  df-dm 5660  df-rn 5661

This theorem is used by:  ima0  6074  rnxpid  6164  xpima  6173  0ima  6200  f0  6763  rnfvprc  6879  2ndval  8004  frxp  8140  oarec  8573  fodomr  9150  fodomfir  9322  dfac5lem3  10207  itunitc  10502  relexprnd  15206  0rest  17605  arwval  18223  psgnsn  19739  oppglsm  19861  mpfrcl  22399  ply1frcl  22641  edgval  29632  0grsubgr  29864  0uhgrsubgr  29865  0ngrp  31118  bafval  31211  tocycf  33724  tocyc01  33725  domnprodeq0  33886  unitprodclb  33990  locfinref  34519  esumrnmpt2  34746  sibf0  35012  mvtval  36351  mrsubvrs  36373  mstaval  36395  mzpmfp  43851  dmnonrel  44683  imanonrel  44686  conrel1d  44756  clsneibex  45195  neicvgbex  45205  sge00  47479  dmrnxp  50041