Theorem rn0 5086

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 5042	. 2 |- dom (/) = (/)
2		dm0rn0 5045	. 2 |- ( dom (/) = (/) <-> ran (/) = (/) )
3	1, 2	mpbi 200	1 |- ran (/) = (/)

Syntax hints:   = wceq 1649   (/)c0 3588   dom cdm 4837   ran crn 4838

This theorem is referenced by:  ima0  5180  0ima  5181  rnxpid  5261  xpima  5272  f0  5586  2ndval  6311  frxp  6415  oarec  6764  map0e  7010  fodomr  7217  dfac5lem3  7962  itunitc  8257  0rest  13612  arwval  14153  oppglsm  15231  mpfrcl  19892  nbgra0edg  21397  uvtx01vtx  21454  0ngrp  21752  bafval  22036  sibf0  24602  mzpmfp  26694  pmtrfrn  27268

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-cnv 4845  df-dm 4847  df-rn 4848