Theorem dm0rn0 5206

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 1599	. . . . . 6 |- ( A. x -. E. y x A y <-> -. E. x E. y x A y )
2		excom 1833	. . . . . 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 1599	. . . . 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 3772	. . . . . 6 |- -. x e. (/)
7	6	nbn 347	. . . . 5 |- ( -. E. y x A y <-> ( E. y x A y <-> x e. (/) ) )
8	7	albii 1625	. . . 4 |- ( A. x -. E. y x A y <-> A. x ( E. y x A y <-> x e. (/) ) )
9		noel 3772	. . . . . 6 |- -. y e. (/)
10	9	nbn 347	. . . . 5 |- ( -. E. x x A y <-> ( E. x x A y <-> y e. (/) ) )
11	10	albii 1625	. . . 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 2566	. . 3 |- ( { x | E. y x A y } = (/) <-> A. x ( E. y x A y <-> x e. (/) ) )
14		abeq1 2566	. . 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 4996	. . 3 |- dom A = { x | E. y x A y }
17	16	eqeq1i 2448	. 2 |- ( dom A = (/) <-> { x | E. y x A y } = (/) )
18		dfrn2 5178	. . 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 1379   = wceq 1381   E.wex 1597   e. wcel 1802   {cab 2426   (/)c0 3768   class class class wbr 4434   dom cdm 4986   ran crn 4987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4555  ax-nul 4563  ax-pr 4673

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-rab 2800  df-v 3095  df-dif 3462  df-un 3464  df-in 3466  df-ss 3473  df-nul 3769  df-if 3924  df-sn 4012  df-pr 4014  df-op 4018  df-br 4435  df-opab 4493  df-cnv 4994  df-dm 4996  df-rn 4997

This theorem is referenced by:  rn0  5241  relrn0  5247  imadisj  5343  ndmima  5360  rnsnn0  5461  f00  5754  f0rn0  5757  2nd0  6789  iinon  7010  onoviun  7013  onnseq  7014  map0b  7456  fodomfib  7799  intrnfi  7875  wdomtr  8001  noinfep  8076  noinfepOLD  8077  wemapwe  8139  wemapweOLD  8140  fin23lem31  8723  fin23lem40  8731  isf34lem7  8759  isf34lem6  8760  ttukeylem6  8894  fodomb  8904  rpnnen1lem4  11217  rpnnen1lem5  11218  fseqsupcl  12063  fseqsupubi  12064  ruclem11  13847  prmreclem6  14313  0ram  14412  0ram2  14413  0ramcl  14415  gsumval2  15778  ghmrn  16151  gexex  16730  gsumval3OLD  16779  gsumval3  16782  iinopn  19281  hauscmplem  19776  fbasrn  20255  alexsublem  20414  evth  21329  minveclem1  21709  minveclem3b  21713  ovollb2  21770  ovolunlem1a  21777  ovolunlem1  21778  ovoliunlem1  21783  ovoliun2  21787  ioombl1lem4  21841  uniioombllem1  21860  uniioombllem2  21862  uniioombllem6  21867  mbfsup  21941  mbfinf  21942  mbflimsup  21943  itg1climres  21991  itg2monolem1  22027  itg2mono  22030  itg2i1fseq2  22033  itg2cnlem1  22038  minvecolem1  25659  rge0scvg  27801  esumpcvgval  27954  cvmsss2  28589  fin2so  30012  heicant  30021  isbnd3  30252  totbndbnd  30257  stoweidlem35  31706