Theorem noel 3555

Description: The empty set has no elements. Theorem 6.14 of [Quine] p. 44. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 1-Sep-2015.)

Assertion

Ref	Expression
noel	⊢ ¬ A ∈ ∅

Proof of Theorem noel

Step	Hyp	Ref	Expression
1		eldifi 3389	. . 3 ⊢ (A ∈ (V ∖ V) → A ∈ V)
2		eldifn 3390	. . 3 ⊢ (A ∈ (V ∖ V) → ¬ A ∈ V)
3	1, 2	pm2.65i 165	. 2 ⊢ ¬ A ∈ (V ∖ V)
4		df-nul 3552	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2417	. 2 ⊢ (A ∈ ∅ ↔ A ∈ (V ∖ V))
6	3, 5	mtbir 290	1 ⊢ ¬ A ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 1710  Vcvv 2860   ∖ cdif 3207  ∅c0 3551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-dif 3216  df-nul 3552

This theorem is referenced by:  n0i  3556  n0f  3559  rex0  3564  abvor0  3568  rab0  3572  un0  3576  in0  3577  0ss  3580  r19.2zb  3641  ral0  3655  int0  3941  iun0  4023  0iun  4024  vinf  4556  xp0r  4843  dm0  4919  dm0rn0  4922  dmeq0  4923  cnv0  5032  co02  5093  co01  5094  fv01  5355  clos10  5888  po0  5940  connex0  5941