Theorem noel 2879

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 1884	. . . . 5 |- x = x
2		dfnul2 2877	. . . . . . 7 |- (/) = {x | -. x = x}
3	2	abeq2i 2001	. . . . . 6 |- (x e. (/) <-> -. x = x)
4	3	con2bii 238	. . . . 5 |- (x = x <-> -. x e. (/))
5	1, 4	mpbi 206	. . . 4 |- -. x e. (/)
6		eleq1 1957	. . . 4 |- (x = A -> (x e. (/) <-> A e. (/)))
7	5, 6	mtbii 784	. . 3 |- (x = A -> -. A e. (/))
8	7	vtocleg 2355	. 2 |- (A e. _V -> -. A e. (/))
9		elisset 2299	. . 3 |- (A e. (/) -> A e. _V)
10	9	con3i 114	. 2 |- (-. A e. _V -> -. A e. (/))
11	8, 10	pm2.61i 140	1 |- -. A e. (/)

Syntax hints:  -. wn 2   = wceq 1298   e. wcel 1300  _Vcvv 2292  (/)c0 2875

This theorem is referenced by:  n0i 2880  ne0f 2883  rex0 2888  rab0 2894  rab0OLD 2895  un0 2896  in0 2897  0ss 2900  disj 2914  r19.2zb 2959  rzalOLD 2971  ral0 2974  disjsnOLD 3090  int0 3230  iun0 3309  iun0OLD 3310  0iun 3311  0iunOLD 3312  po0OLD 3602  so0OLD 3622  ord0eln0 3717  nlim0 3721  nsuceq0 3749  xp0r 4065  0nelxp 4066  dm0 4170  dm0OLD 4171  dm0rn0 4175  reldm0 4176  elimasni 4292  intirrOLD 4313  cnv0 4319  co02 4411  fn0OLD 4533  omordi 5245  omsmolem 5313  ixp0 5420  en3lp 5758  rankr1 5785  zorn2lem7 5956  brdom3 5963  alephordi 6022  nlt1pi 6185  elioo3g 7547  elioore 7554  elfz2 7642  om2uzlti 7709  ntreq0 8984  helloworld 10144  emnfil 10273  extbas1 10291  elioo1t3 14846  empntop 14857  hmeogrp 14892  altretop 14997  0ded 15104  0cat 15105  filssufillem 15570  flimcls 15588  en3lpVD 16669

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-dif 2597  df-nul 2876

Copyright terms: Public domain