Theorem dm0rn0 5132

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 1622	. . . . . 6 |- ( A. x -. E. y x A y <-> -. E. x E. y x A y )
2		excom 1857	. . . . . 6 |- ( E. x E. y x A y <-> E. y E. x x A y )
3	1, 2	xchbinx 308	. . . . 5 |- ( A. x -. E. y x A y <-> -. E. y E. x x A y )
4		alnex 1622	. . . . 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 3715	. . . . . 6 |- -. x e. (/)
7	6	nbn 345	. . . . 5 |- ( -. E. y x A y <-> ( E. y x A y <-> x e. (/) ) )
8	7	albii 1648	. . . 4 |- ( A. x -. E. y x A y <-> A. x ( E. y x A y <-> x e. (/) ) )
9		noel 3715	. . . . . 6 |- -. y e. (/)
10	9	nbn 345	. . . . 5 |- ( -. E. x x A y <-> ( E. x x A y <-> y e. (/) ) )
11	10	albii 1648	. . . 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 2507	. . 3 |- ( { x | E. y x A y } = (/) <-> A. x ( E. y x A y <-> x e. (/) ) )
14		abeq1 2507	. . 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 4923	. . 3 |- dom A = { x | E. y x A y }
17	16	eqeq1i 2389	. 2 |- ( dom A = (/) <-> { x | E. y x A y } = (/) )
18		dfrn2 5104	. . 3 |- ran A = { y | E. x x A y }
19	18	eqeq1i 2389	. 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 1397   = wceq 1399   E.wex 1620   e. wcel 1826   {cab 2367   (/)c0 3711   class class class wbr 4367   dom cdm 4913   ran crn 4914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-br 4368  df-opab 4426  df-cnv 4921  df-dm 4923  df-rn 4924

This theorem is referenced by:  rn0  5167  relrn0  5173  imadisj  5268  ndmimaOLD  5286  rnsnn0  5382  f00  5675  f0rn0  5678  2nd0  6706  iinon  6929  onoviun  6932  onnseq  6933  map0b  7376  fodomfib  7715  intrnfi  7791  wdomtr  7916  noinfep  7990  wemapwe  8052  wemapweOLD  8053  fin23lem31  8636  fin23lem40  8644  isf34lem7  8672  isf34lem6  8673  ttukeylem6  8807  fodomb  8817  rpnnen1lem4  11130  rpnnen1lem5  11131  fseqsupcl  11990  fseqsupubi  11991  dmtrclfv  12856  ruclem11  13975  prmreclem6  14441  0ram  14540  0ram2  14541  0ramcl  14543  gsumval2  16024  ghmrn  16397  gexex  16976  gsumval3OLD  17025  gsumval3  17028  iinopn  19496  hauscmplem  19992  fbasrn  20470  alexsublem  20629  evth  21544  minveclem1  21924  minveclem3b  21928  ovollb2  21985  ovolunlem1a  21992  ovolunlem1  21993  ovoliunlem1  21998  ovoliun2  22002  ioombl1lem4  22056  uniioombllem1  22075  uniioombllem2  22077  uniioombllem6  22082  mbfsup  22156  mbfinf  22157  mbflimsup  22158  itg1climres  22206  itg2monolem1  22242  itg2mono  22245  itg2i1fseq2  22248  itg2cnlem1  22253  minvecolem1  25907  rge0scvg  28085  esumpcvgval  28226  cvmsss2  28908  fin2so  30205  heicant  30214  isbnd3  30446  totbndbnd  30451  stoweidlem35  31983