Theorem dm0rn0 5068

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 1662	. . . . . 6 |- ( A. x -. E. y x A y <-> -. E. x E. y x A y )
2		excom 1900	. . . . . 6 |- ( E. x E. y x A y <-> E. y E. x x A y )
3	1, 2	xchbinx 312	. . . . 5 |- ( A. x -. E. y x A y <-> -. E. y E. x x A y )
4		alnex 1662	. . . . 5 |- ( A. y -. E. x x A y <-> -. E. y E. x x A y )
5	3, 4	bitr4i 256	. . . 4 |- ( A. x -. E. y x A y <-> A. y -. E. x x A y )
6		noel 3766	. . . . . 6 |- -. x e. (/)
7	6	nbn 349	. . . . 5 |- ( -. E. y x A y <-> ( E. y x A y <-> x e. (/) ) )
8	7	albii 1688	. . . 4 |- ( A. x -. E. y x A y <-> A. x ( E. y x A y <-> x e. (/) ) )
9		noel 3766	. . . . . 6 |- -. y e. (/)
10	9	nbn 349	. . . . 5 |- ( -. E. x x A y <-> ( E. x x A y <-> y e. (/) ) )
11	10	albii 1688	. . . 4 |- ( A. y -. E. x x A y <-> A. y ( E. x x A y <-> y e. (/) ) )
12	5, 8, 11	3bitr3i 279	. . 3 |- ( A. x ( E. y x A y <-> x e. (/) ) <-> A. y ( E. x x A y <-> y e. (/) ) )
13		abeq1 2548	. . 3 |- ( { x | E. y x A y } = (/) <-> A. x ( E. y x A y <-> x e. (/) ) )
14		abeq1 2548	. . 3 |- ( { y | E. x x A y } = (/) <-> A. y ( E. x x A y <-> y e. (/) ) )
15	12, 13, 14	3bitr4i 281	. 2 |- ( { x | E. y x A y } = (/) <-> { y | E. x x A y } = (/) )
16		df-dm 4861	. . 3 |- dom A = { x | E. y x A y }
17	16	eqeq1i 2430	. 2 |- ( dom A = (/) <-> { x | E. y x A y } = (/) )
18		dfrn2 5040	. . 3 |- ran A = { y | E. x x A y }
19	18	eqeq1i 2430	. 2 |- ( ran A = (/) <-> { y | E. x x A y } = (/) )
20	15, 17, 19	3bitr4i 281	1 |- ( dom A = (/) <-> ran A = (/) )

Syntax hints:   -. wn 3   <-> wb 188   A.wal 1436   = wceq 1438   E.wex 1660   e. wcel 1869   {cab 2408   (/)c0 3762   class class class wbr 4421   dom cdm 4851   ran crn 4852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-rab 2785  df-v 3084  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-br 4422  df-opab 4481  df-cnv 4859  df-dm 4861  df-rn 4862

This theorem is referenced by:  rn0  5103  relrn0  5109  imadisj  5204  ndmimaOLD  5223  rnsnn0  5319  f00  5780  f0rn0  5783  2nd0  6812  iinon  7065  onoviun  7068  onnseq  7069  map0b  7516  fodomfib  7855  intrnfi  7934  wdomtr  8094  noinfep  8168  wemapwe  8205  fin23lem31  8775  fin23lem40  8783  isf34lem7  8811  isf34lem6  8812  ttukeylem6  8946  fodomb  8956  rpnnen1lem4  11295  rpnnen1lem5  11296  fseqsupcl  12191  fseqsupubi  12192  dmtrclfv  13076  ruclem11  14285  prmreclem6  14858  0ram  14971  0ram2  14972  0ramcl  14974  gsumval2  16516  ghmrn  16889  gexex  17484  gsumval3  17534  iinopn  19924  hauscmplem  20413  fbasrn  20891  alexsublem  21051  evth  21979  minveclem1  22358  minveclem3b  22362  minveclem3bOLD  22374  ovollb2  22434  ovolunlem1a  22441  ovolunlem1  22442  ovoliunlem1  22447  ovoliun2  22451  ioombl1lem4  22506  uniioombllem1  22530  uniioombllem2  22532  uniioombllem2OLD  22533  uniioombllem6  22538  mbfsup  22612  mbfinf  22613  mbfinfOLD  22614  mbflimsup  22615  mbflimsupOLD  22616  itg1climres  22664  itg2monolem1  22700  itg2mono  22703  itg2i1fseq2  22706  itg2cnlem1  22711  minvecolem1  26508  rge0scvg  28757  esumpcvgval  28901  cvmsss2  29999  fin2so  31890  ptrecube  31898  heicant  31933  isbnd3  32074  totbndbnd  32079  stoweidlem35  37760  hoicvr  38189