Theorem noel 2281

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

Assertion

Ref	Expression
noel	⊢ ¬ A ∈ ∅

Proof of Theorem noel

Step	Hyp	Ref	Expression
1		eqid 1474	. . . . 5 ⊢ x = x
2		dfnul2 2279	. . . . . . 7 ⊢ ∅ = {x∣ ¬ x = x}
3	2	abeq2i 1568	. . . . . 6 ⊢ (x ∈ ∅ ↔ ¬ x = x)
4	3	con2bii 221	. . . . 5 ⊢ (x = x ↔ ¬ x ∈ ∅)
5	1, 4	mpbi 189	. . . 4 ⊢ ¬ x ∈ ∅
6		eleq1 1532	. . . 4 ⊢ (x = A → (x ∈ ∅ ↔ A ∈ ∅))
7	5, 6	mtbii 715	. . 3 ⊢ (x = A → ¬ A ∈ ∅)
8	7	vtocleg 1852	. 2 ⊢ (A ∈ V → ¬ A ∈ ∅)
9		elisset 1814	. . 3 ⊢ (A ∈ ∅ → A ∈ V)
10	9	con3i 98	. 2 ⊢ (¬ A ∈ V → ¬ A ∈ ∅)
11	8, 10	pm2.61i 126	1 ⊢ ¬ A ∈ ∅

Syntax hints:  ¬ wn 2   = wceq 955   ∈ wcel 957  Vcvv 1808  ∅c0 2277

This theorem is referenced by:  n0i 2282  ne0f 2284  rex0 2288  rab0 2290  un0 2294  in0 2295  0ss 2298  disj 2308  rzal 2352  ral0 2355  disjsn 2438  int0 2543  iun0 2600  0iun 2601  po0 2845  so0 2861  ord0eln0 3019  nsuceq0 3049  xp0r 3235  0nelxp 3236  dm0 3319  dm0rn0 3326  reldm0 3327  intirr 3437  cnv0 3442  co02 3504  fn0 3601  omordi 4190  omsmolem 4249  ixp0 4354  rankr1 4657  zorn2lem7 4777  brdom3 4784  alephordi 4857  nlt1pi 5016  om2uzlt 6248  elioo3g 6330  elfz2t 6417  ntreq0 7668  helloworld 8741  elioo1t3 10442  empntop 10452  hmeogrp 10484  emnfil 10499  0ded 10606  0cat 10607

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809  df-dif 2046  df-nul 2278

Copyright terms: Public domain