Theorem dm0 3312

Description: The domain of the empty set is empty. Part of Theorem 3.8(v) of [Monk1] p. 36.

Assertion

Ref	Expression
dm0	|- dom (/) = (/)

Proof of Theorem dm0

Step	Hyp	Ref	Expression
1		noel 2274	. . . . 5 |- -. <.x, y>. e. (/)
2	1	nex 1097	. . . 4 |- -. E.y<.x, y>. e. (/)
3		eqid 1468	. . . . 5 |- x = x
4	3	negbi 87	. . . 4 |- -. -. x = x
5	2, 4	2false 717	. . 3 |- (E.y<.x, y>. e. (/) <-> -. x = x)
6	5	abbii 1567	. 2 |- {x | E.y<.x, y>. e. (/)} = {x | -. x = x}
7		dfdm3 3291	. 2 |- dom (/) = {x | E.y<.x, y>. e. (/)}
8		dfnul2 2272	. 2 |- (/) = {x | -. x = x}
9	6, 7, 8	3eqtr4 1497	1 |- dom (/) = (/)

Syntax hints:  -. wn 2   = wceq 953   e. wcel 955  E.wex 977  {cab 1456  (/)c0 2270  <.cop 2401  dom cdm 3160

This theorem is referenced by:  dmxpid 3322  rn0 3341  dmxpss 3459  fn0 3591  f1o00 3699  tz7.44lem1 3912  tz7.44-2 3914  dfrdg2 3918  1stval 4065  infxpidmlem4 7498  0met 7765  dmadjrnb 9747  0alg 10533  0ded 10534  0cat 10535

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-dif 2039  df-nul 2271  df-br 2610  df-dm 3178

Copyright terms: Public domain