Theorem noel 2336

Description: The empty set has no elements. Theorem 6.14 of [Quine] p. 44.

Assertion

Ref	Expression
noel	|- -. A e. (/)

Proof of Theorem noel

Step	Hyp	Ref	Expression
1		eqid 1518	. . . . 5 |- x = x
2		dfnul2 2334	. . . . . . 7 |- (/) = {x | -. x = x}
3	2	abeq2i 1613	. . . . . 6 |- (x e. (/) <-> -. x = x)
4	3	con2bii 219	. . . . 5 |- (x = x <-> -. x e. (/))
5	1, 4	mpbi 187	. . . 4 |- -. x e. (/)
6		eleq1 1577	. . . 4 |- (x = A -> (x e. (/) <-> A e. (/)))
7	5, 6	mtbii 721	. . 3 |- (x = A -> -. A e. (/))
8	7	vtocleg 1901	. 2 |- (A e. V -> -. A e. (/))
9		elisset 1863	. . 3 |- (A e. (/) -> A e. V)
10	9	con3i 98	. 2 |- (-. A e. V -> -. A e. (/))
11	8, 10	pm2.61i 124	1 |- -. A e. (/)

Syntax hints:  -. wn 2   = wceq 992   e. wcel 994  Vcvv 1857  (/)c0 2332

This theorem is referenced by:  n0i 2337  ne0f 2340  rex0 2344  rab0 2346  un0 2350  in0 2351  0ss 2354  disj 2364  rzal 2409  ral0 2412  disjsn 2502  int0 2614  iun0 2672  0iun 2673  po0 2927  so0 2944  ord0eln0 3027  nsuceq0 3053  xp0r 3325  0nelxp 3326  dm0 3414  dm0rn0 3417  reldm0 3418  intirr 3533  cnv0 3538  co02 3612  fn0 3711  omordi 4333  omsmolem 4396  ixp0 4502  rankr1 4820  zorn2lem7 4940  brdom3 4947  alephordi 5024  nlt1pi 5187  elioo3g 6506  elioore 6512  elfz2 6600  om2uzlti 6661  ntreq0 7918  helloworld 9060  elioo1t3 10996  empntop 11007  hmeogrp 11044  emnfil 11078  altretop 11144  0ded 11211  0cat 11212  r19.2zb 11393  extbas1 11641  filssufillem 11655  flimcls 11684

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-dif 2101  df-nul 2333

Copyright terms: Public domain