Theorem dm0rn0 5057

Description: An empty domain implies an empty range. (Contributed by NM, 21-May-1998.)

Assertion

Ref	Expression
dm0rn0	|- ( dom A = (/) <-> ran A = (/) )

Proof of Theorem dm0rn0

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		alnex 1673	. . . . . 6 |- ( A. x -. E. y x A y <-> -. E. x E. y x A y )
2		excom 1944	. . . . . 6 |- ( E. x E. y x A y <-> E. y E. x x A y )
3	1, 2	xchbinx 317	. . . . 5 |- ( A. x -. E. y x A y <-> -. E. y E. x x A y )
4		alnex 1673	. . . . 5 |- ( A. y -. E. x x A y <-> -. E. y E. x x A y )
5	3, 4	bitr4i 260	. . . 4 |- ( A. x -. E. y x A y <-> A. y -. E. x x A y )
6		noel 3726	. . . . . 6 |- -. x e. (/)
7	6	nbn 354	. . . . 5 |- ( -. E. y x A y <-> ( E. y x A y <-> x e. (/) ) )
8	7	albii 1699	. . . 4 |- ( A. x -. E. y x A y <-> A. x ( E. y x A y <-> x e. (/) ) )
9		noel 3726	. . . . . 6 |- -. y e. (/)
10	9	nbn 354	. . . . 5 |- ( -. E. x x A y <-> ( E. x x A y <-> y e. (/) ) )
11	10	albii 1699	. . . 4 |- ( A. y -. E. x x A y <-> A. y ( E. x x A y <-> y e. (/) ) )
12	5, 8, 11	3bitr3i 283	. . 3 |- ( A. x ( E. y x A y <-> x e. (/) ) <-> A. y ( E. x x A y <-> y e. (/) ) )
13		abeq1 2581	. . 3 |- ( { x | E. y x A y } = (/) <-> A. x ( E. y x A y <-> x e. (/) ) )
14		abeq1 2581	. . 3 |- ( { y | E. x x A y } = (/) <-> A. y ( E. x x A y <-> y e. (/) ) )
15	12, 13, 14	3bitr4i 285	. 2 |- ( { x | E. y x A y } = (/) <-> { y | E. x x A y } = (/) )
16		df-dm 4849	. . 3 |- dom A = { x | E. y x A y }
17	16	eqeq1i 2476	. 2 |- ( dom A = (/) <-> { x | E. y x A y } = (/) )
18		dfrn2 5028	. . 3 |- ran A = { y | E. x x A y }
19	18	eqeq1i 2476	. 2 |- ( ran A = (/) <-> { y | E. x x A y } = (/) )
20	15, 17, 19	3bitr4i 285	1 |- ( dom A = (/) <-> ran A = (/) )

Syntax hints:   -. wn 3   <-> wb 189   A.wal 1450   = wceq 1452   E.wex 1671   e. wcel 1904   {cab 2457   (/)c0 3722   class class class wbr 4395   dom cdm 4839   ran crn 4840

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-br 4396  df-opab 4455  df-cnv 4847  df-dm 4849  df-rn 4850

This theorem is referenced by:  rn0  5092  relrn0  5098  imadisj  5193  ndmimaOLD  5212  rnsnn0  5309  f00  5778  f0rn0  5781  2nd0  6819  iinon  7077  onoviun  7080  onnseq  7081  map0b  7528  fodomfib  7869  intrnfi  7948  wdomtr  8108  noinfep  8183  wemapwe  8220  fin23lem31  8791  fin23lem40  8799  isf34lem7  8827  isf34lem6  8828  ttukeylem6  8962  fodomb  8972  rpnnen1lem4  11316  rpnnen1lem5  11317  fseqsupcl  12228  fseqsupubi  12229  dmtrclfv  13159  ruclem11  14369  prmreclem6  14944  0ram  15057  0ram2  15058  0ramcl  15060  gsumval2  16601  ghmrn  16974  gexex  17569  gsumval3  17619  iinopn  20009  hauscmplem  20498  fbasrn  20977  alexsublem  21137  evth  22065  minveclem1  22444  minveclem3b  22448  minveclem3bOLD  22460  ovollb2  22520  ovolunlem1a  22527  ovolunlem1  22528  ovoliunlem1  22533  ovoliun2  22537  ioombl1lem4  22593  uniioombllem1  22617  uniioombllem2  22619  uniioombllem2OLD  22620  uniioombllem6  22625  mbfsup  22699  mbfinf  22700  mbfinfOLD  22701  mbflimsup  22702  mbflimsupOLD  22703  itg1climres  22751  itg2monolem1  22787  itg2mono  22790  itg2i1fseq2  22793  itg2cnlem1  22798  minvecolem1  26597  rge0scvg  28829  esumpcvgval  28973  cvmsss2  30069  fin2so  31996  ptrecube  32004  heicant  32039  isbnd3  32180  totbndbnd  32185  rnnonrel  36268  stoweidlem35  38008  hoicvr  38488