Theorem rn0 5915

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

This proof depends on syntax axioms:   = wceq 1570  ∅c0 4281  dom cdm 5655  ran crn 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  ima0  6087  rnxpid  6177  xpima  6186  0ima  6213  f0  6785  rnfvprc  6902  2ndval  8028  frxp  8165  oarec  8598  fodomr  9175  fodomfir  9347  dfac5lem3  10231  itunitc  10526  relexprnd  15230  0rest  17629  arwval  18247  psgnsn  19764  oppglsm  19886  mpfrcl  22424  ply1frcl  22666  edgval  29657  0grsubgr  29889  0uhgrsubgr  29890  0ngrp  31143  bafval  31236  tocycf  33748  tocyc01  33749  domnprodeq0  33910  unitprodclb  34014  locfinref  34543  esumrnmpt2  34770  sibf0  35036  mvtval  36432  mrsubvrs  36454  mstaval  36476  mzpmfp  43951  dmnonrel  44782  imanonrel  44785  conrel1d  44855  clsneibex  45294  neicvgbex  45304  sge00  47591  dmrnxp  50153