Theorem noel 2255

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 1452	. . . . 5 |- x = x
2		dfnul2 2253	. . . . . . 7 |- (/) = {x | -. x = x}
3	2	abeq2i 1546	. . . . . 6 |- (x e. (/) <-> -. x = x)
4	3	con2bii 221	. . . . 5 |- (x = x <-> -. x e. (/))
5	1, 4	mpbi 189	. . . 4 |- -. x e. (/)
6		eleq1 1510	. . . 4 |- (x = A -> (x e. (/) <-> A e. (/)))
7	5, 6	mtbii 713	. . 3 |- (x = A -> -. A e. (/))
8	7	vtocleg 1830	. 2 |- (A e. V -> -. A e. (/))
9		elisset 1792	. . 3 |- (A e. (/) -> A e. V)
10	9	con3i 98	. 2 |- (-. A e. V -> -. A e. (/))
11	8, 10	pm2.61i 126	1 |- -. A e. (/)

Syntax hints:  -. wn 2   = wceq 1099   e. wcel 1105  Vcvv 1786  (/)c0 2251

This theorem is referenced by:  n0i 2256  ne0f 2258  rex0 2262  rab0 2264  un0 2268  in0 2269  0ss 2272  disj 2282  rzal 2326  ral0 2329  disjsn 2412  int0 2515  iun0 2572  0iun 2573  po0 2813  so0 2829  ord0eln0 2986  nsuceq0 3016  xp0r 3201  0nelxp 3202  dm0 3280  dm0rn0 3287  reldm0 3288  intirr 3390  cnv0 3395  co02 3450  fn0 3545  omordi 4135  omsmolem 4194  ixp0 4299  rankr1 4598  zorn2lem7 4718  brdom3 4725  alephordi 4797  nlt1pi 4956  om2uzlt 6186  elioo3g 6268  elfz2t 6355  ntreq0 7599  elioo1t3 8740  hmeogrp 8776  emnfil 8790  0ded 8884  0cat 8885  helloworld 8966

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449  df-v 1787  df-dif 2020  df-nul 2252

Copyright terms: Public domain