MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rn0 Structured version   Visualization version   GIF version

Theorem rn0 5789
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
StepHypRef Expression
1 dm0 5783 . 2 dom ∅ = ∅
2 dm0rn0 5788 . 2 (dom ∅ = ∅ ↔ ran ∅ = ∅)
31, 2mpbi 232 1 ran ∅ = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1531  c0 4289  dom cdm 5548  ran crn 5549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5058  df-opab 5120  df-cnv 5556  df-dm 5558  df-rn 5559
This theorem is referenced by:  ima0  5938  0ima  5939  rnxpid  6023  xpima  6032  f0  6553  rnfvprc  6657  2ndval  7684  frxp  7812  oarec  8180  fodomr  8660  dfac5lem3  9543  itunitc  9835  0rest  16695  arwval  17295  psgnsn  18640  oppglsm  18759  mpfrcl  20290  ply1frcl  20473  edgval  26826  0grsubgr  27052  0uhgrsubgr  27053  0ngrp  28280  bafval  28373  tocycf  30752  tocyc01  30753  locfinref  31098  esumrnmpt2  31320  sibf0  31585  mvtval  32740  mrsubvrs  32762  mstaval  32784  mzpmfp  39334  dmnonrel  39940  imanonrel  39943  conrel1d  39998  clsneibex  40442  neicvgbex  40452  sge00  42648
  Copyright terms: Public domain W3C validator