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

Theorem rn0 5366
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 5328 . 2 dom ∅ = ∅
2 dm0rn0 5331 . 2 (dom ∅ = ∅ ↔ ran ∅ = ∅)
31, 2mpbi 220 1 ran ∅ = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481  c0 3907  dom cdm 5104  ran crn 5105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-cnv 5112  df-dm 5114  df-rn 5115
This theorem is referenced by:  ima0  5469  0ima  5470  rnxpid  5555  xpima  5564  f0  6073  2ndval  7156  frxp  7272  oarec  7627  fodomr  8096  dfac5lem3  8933  itunitc  9228  0rest  16071  arwval  16674  pmtrfrn  17859  psgnsn  17921  oppglsm  18038  mpfrcl  19499  ply1frcl  19664  edgval  25922  0grsubgr  26151  0uhgrsubgr  26152  0ngrp  27335  bafval  27429  locfinref  29882  esumrnmpt2  30104  sibf0  30370  mvtval  31371  mrsubrn  31384  mrsub0  31387  mrsubf  31388  mrsubccat  31389  mrsubcn  31390  mrsubco  31392  mrsubvrs  31393  elmsubrn  31399  msubrn  31400  msubf  31403  mstaval  31415  mzpmfp  37129  dmnonrel  37715  imanonrel  37718  conrel1d  37774  clsneibex  38220  neicvgbex  38230  sge00  40356
  Copyright terms: Public domain W3C validator