Theorem dm0rn0 5054

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 1588	. . . . . 6 |- ( A. x -. E. y x A y <-> -. E. x E. y x A y )
2		excom 1787	. . . . . 6 |- ( E. x E. y x A y <-> E. y E. x x A y )
3	1, 2	xchbinx 310	. . . . 5 |- ( A. x -. E. y x A y <-> -. E. y E. x x A y )
4		alnex 1588	. . . . 5 |- ( A. y -. E. x x A y <-> -. E. y E. x x A y )
5	3, 4	bitr4i 252	. . . 4 |- ( A. x -. E. y x A y <-> A. y -. E. x x A y )
6		noel 3639	. . . . . 6 |- -. x e. (/)
7	6	nbn 347	. . . . 5 |- ( -. E. y x A y <-> ( E. y x A y <-> x e. (/) ) )
8	7	albii 1610	. . . 4 |- ( A. x -. E. y x A y <-> A. x ( E. y x A y <-> x e. (/) ) )
9		noel 3639	. . . . . 6 |- -. y e. (/)
10	9	nbn 347	. . . . 5 |- ( -. E. x x A y <-> ( E. x x A y <-> y e. (/) ) )
11	10	albii 1610	. . . 4 |- ( A. y -. E. x x A y <-> A. y ( E. x x A y <-> y e. (/) ) )
12	5, 8, 11	3bitr3i 275	. . 3 |- ( A. x ( E. y x A y <-> x e. (/) ) <-> A. y ( E. x x A y <-> y e. (/) ) )
13		abeq1 2547	. . 3 |- ( { x | E. y x A y } = (/) <-> A. x ( E. y x A y <-> x e. (/) ) )
14		abeq1 2547	. . 3 |- ( { y | E. x x A y } = (/) <-> A. y ( E. x x A y <-> y e. (/) ) )
15	12, 13, 14	3bitr4i 277	. 2 |- ( { x | E. y x A y } = (/) <-> { y | E. x x A y } = (/) )
16		df-dm 4848	. . 3 |- dom A = { x | E. y x A y }
17	16	eqeq1i 2448	. 2 |- ( dom A = (/) <-> { x | E. y x A y } = (/) )
18		dfrn2 5026	. . 3 |- ran A = { y | E. x x A y }
19	18	eqeq1i 2448	. 2 |- ( ran A = (/) <-> { y | E. x x A y } = (/) )
20	15, 17, 19	3bitr4i 277	1 |- ( dom A = (/) <-> ran A = (/) )

Syntax hints:   -. wn 3   <-> wb 184   A.wal 1367   = wceq 1369   E.wex 1586   e. wcel 1756   {cab 2427   (/)c0 3635   class class class wbr 4290   dom cdm 4838   ran crn 4839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422  ax-sep 4411  ax-nul 4419  ax-pr 4529

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-rab 2722  df-v 2972  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-nul 3636  df-if 3790  df-sn 3876  df-pr 3878  df-op 3882  df-br 4291  df-opab 4349  df-cnv 4846  df-dm 4848  df-rn 4849

This theorem is referenced by:  rn0  5089  relrn0  5095  imadisj  5186  ndmima  5203  rnsnn0  5303  f00  5591  2nd0  6582  iinon  6799  onoviun  6802  onnseq  6803  map0b  7249  fodomfib  7589  intrnfi  7664  wdomtr  7788  noinfep  7863  noinfepOLD  7864  wemapwe  7926  wemapweOLD  7927  fin23lem31  8510  fin23lem40  8518  isf34lem7  8546  isf34lem6  8547  ttukeylem6  8681  fodomb  8691  rpnnen1lem4  10980  rpnnen1lem5  10981  fseqsupcl  11797  fseqsupubi  11798  ruclem11  13520  prmreclem6  13980  0ram  14079  0ram2  14080  0ramcl  14082  gsumval2  15511  ghmrn  15758  gexex  16333  gsumval3OLD  16380  gsumval3  16383  iinopn  18513  hauscmplem  19007  fbasrn  19455  alexsublem  19614  evth  20529  minveclem1  20909  minveclem3b  20913  ovollb2  20970  ovolunlem1a  20977  ovolunlem1  20978  ovoliunlem1  20983  ovoliun2  20987  ioombl1lem4  21040  uniioombllem1  21059  uniioombllem2  21061  uniioombllem6  21066  mbfsup  21140  mbfinf  21141  mbflimsup  21142  itg1climres  21190  itg2monolem1  21226  itg2mono  21229  itg2i1fseq2  21232  itg2cnlem1  21237  minvecolem1  24273  rge0scvg  26377  esumpcvgval  26525  cvmsss2  27161  fin2so  28413  heicant  28423  isbnd3  28680  totbndbnd  28685  stoweidlem35  29827  f0rn0  30138