Theorem rn0 5102

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 5064	. 2 |- dom (/) = (/)
2		dm0rn0 5067	. 2 |- ( dom (/) = (/) <-> ran (/) = (/) )
3	1, 2	mpbi 211	1 |- ran (/) = (/)

Syntax hints:   = wceq 1437   (/)c0 3761   dom cdm 4850   ran crn 4851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421  df-opab 4480  df-cnv 4858  df-dm 4860  df-rn 4861

This theorem is referenced by:  ima0  5199  0ima  5200  rnxpid  5286  xpima  5295  f0  5778  2ndval  6807  frxp  6914  oarec  7268  fodomr  7726  dfac5lem3  8557  itunitc  8852  0rest  15316  arwval  15926  pmtrfrn  17087  psgnsn  17149  oppglsm  17282  mpfrcl  18729  ply1frcl  18895  nbgra0edg  25146  uvtx01vtx  25206  rusgra0edg  25669  0ngrp  25925  bafval  26209  locfinref  28664  esumrnmpt2  28885  sibf0  29163  mvtval  30134  mrsubrn  30147  mrsub0  30150  mrsubf  30151  mrsubccat  30152  mrsubcn  30153  mrsubco  30155  mrsubvrs  30156  elmsubrn  30162  msubrn  30163  msubf  30166  mstaval  30178  mzpmfp  35508  conrel1d  36115  sge00  38006