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 1667	. . . . . 6 |- ( A. x -. E. y x A y <-> -. E. x E. y x A y )
2		excom 1929	. . . . . 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 1667	. . . . 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 3737	. . . . . 6 |- -. x e. (/)
7	6	nbn 349	. . . . 5 |- ( -. E. y x A y <-> ( E. y x A y <-> x e. (/) ) )
8	7	albii 1693	. . . 4 |- ( A. x -. E. y x A y <-> A. x ( E. y x A y <-> x e. (/) ) )
9		noel 3737	. . . . . 6 |- -. y e. (/)
10	9	nbn 349	. . . . 5 |- ( -. E. x x A y <-> ( E. x x A y <-> y e. (/) ) )
11	10	albii 1693	. . . 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 2563	. . 3 |- ( { x | E. y x A y } = (/) <-> A. x ( E. y x A y <-> x e. (/) ) )
14		abeq1 2563	. . 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 4847	. . 3 |- dom A = { x | E. y x A y }
17	16	eqeq1i 2458	. 2 |- ( dom A = (/) <-> { x | E. y x A y } = (/) )
18		dfrn2 5026	. . 3 |- ran A = { y | E. x x A y }
19	18	eqeq1i 2458	. 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 1444   = wceq 1446   E.wex 1665   e. wcel 1889   {cab 2439   (/)c0 3733   class class class wbr 4405   dom cdm 4837   ran crn 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-rab 2748  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-br 4406  df-opab 4465  df-cnv 4845  df-dm 4847  df-rn 4848

This theorem is referenced by:  rn0  5089  relrn0  5095  imadisj  5190  ndmimaOLD  5209  rnsnn0  5305  f00  5770  f0rn0  5773  2nd0  6805  iinon  7064  onoviun  7067  onnseq  7068  map0b  7515  fodomfib  7856  intrnfi  7935  wdomtr  8095  noinfep  8170  wemapwe  8207  fin23lem31  8778  fin23lem40  8786  isf34lem7  8814  isf34lem6  8815  ttukeylem6  8949  fodomb  8959  rpnnen1lem4  11300  rpnnen1lem5  11301  fseqsupcl  12197  fseqsupubi  12198  dmtrclfv  13094  ruclem11  14304  prmreclem6  14877  0ram  14990  0ram2  14991  0ramcl  14993  gsumval2  16535  ghmrn  16908  gexex  17503  gsumval3  17553  iinopn  19944  hauscmplem  20433  fbasrn  20911  alexsublem  21071  evth  21999  minveclem1  22378  minveclem3b  22382  minveclem3bOLD  22394  ovollb2  22454  ovolunlem1a  22461  ovolunlem1  22462  ovoliunlem1  22467  ovoliun2  22471  ioombl1lem4  22526  uniioombllem1  22550  uniioombllem2  22552  uniioombllem2OLD  22553  uniioombllem6  22558  mbfsup  22632  mbfinf  22633  mbfinfOLD  22634  mbflimsup  22635  mbflimsupOLD  22636  itg1climres  22684  itg2monolem1  22720  itg2mono  22723  itg2i1fseq2  22726  itg2cnlem1  22731  minvecolem1  26528  rge0scvg  28767  esumpcvgval  28911  cvmsss2  30009  fin2so  31944  ptrecube  31952  heicant  31987  isbnd3  32128  totbndbnd  32133  rnnonrel  36209  stoweidlem35  37906  hoicvr  38380