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

Theorem rn0 5527
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 5489 . 2 dom ∅ = ∅
2 dm0rn0 5492 . 2 (dom ∅ = ∅ ↔ ran ∅ = ∅)
31, 2mpbi 221 1 ran ∅ = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1634  c0 4073  dom cdm 5263  ran crn 5264
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-sep 4928  ax-nul 4936  ax-pr 5048
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-rab 3073  df-v 3357  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-sn 4327  df-pr 4329  df-op 4333  df-br 4798  df-opab 4860  df-cnv 5271  df-dm 5273  df-rn 5274
This theorem is referenced by:  ima0  5632  0ima  5633  rnxpid  5719  xpima  5728  f0  6241  rnfvprc  6342  2ndval  7339  frxp  7459  oarec  7817  fodomr  8288  dfac5lem3  9169  itunitc  9466  0rest  16318  arwval  16920  psgnsn  18167  oppglsm  18284  mpfrcl  19753  ply1frcl  19918  edgval  26183  0grsubgr  26414  0uhgrsubgr  26415  0ngrp  27722  bafval  27816  locfinref  30265  esumrnmpt2  30487  sibf0  30753  mvtval  31752  mrsubvrs  31774  mstaval  31796  mzpmfp  37851  dmnonrel  38436  imanonrel  38439  conrel1d  38495  clsneibex  38940  neicvgbex  38950  sge00  41116
  Copyright terms: Public domain W3C validator