Theorem noel 3228

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	⊢ ¬ 𝐴 ∈ ∅

Proof of Theorem noel

Step	Hyp	Ref	Expression
1		eldifi 3066	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2		eldifn 3067	. . 3 ⊢ (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
3	1, 2	pm2.65i 568	. 2 ⊢ ¬ 𝐴 ∈ (V ∖ V)
4		df-nul 3225	. . 3 ⊢ ∅ = (V ∖ V)
5	4	eleq2i 2104	. 2 ⊢ (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
6	3, 5	mtbir 596	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∈ wcel 1393  Vcvv 2557   ∖ cdif 2914  ∅c0 3224

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-dif 2920  df-nul 3225

This theorem is referenced by:  n0i  3229  n0rf  3233  rex0  3238  eq0  3239  abvor0dc  3242  rab0  3246  un0  3251  in0  3252  0ss  3255  disj  3268  ral0  3322  int0  3629  iun0  3713  0iun  3714  nlim0  4131  nsuceq0g  4155  ordtriexmidlem  4245  ordtriexmidlem2  4246  ordtriexmid  4247  ordtri2or2exmidlem  4251  onsucelsucexmidlem  4254  reg2exmidlema  4259  reg3exmidlemwe  4303  nn0eln0  4341  0xp  4420  dm0  4549  dm0rn0  4552  reldm0  4553  cnv0  4727  co02  4834  0fv  5208  acexmidlema  5503  acexmidlemb  5504  acexmidlemab  5506  mpt20  5574  nnsucelsuc  6070  nnmordi  6089  nnaordex  6100  0er  6140  elni2  6412  nlt1pig  6439  0npr  6581  fzm1  8962  frec2uzltd  9189  bdcnul  9985  bj-nnelirr  10078