Theorem noel 3636

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

Assertion

Ref	Expression
noel	|- -. A e. (/)

Proof of Theorem noel

Step	Hyp	Ref	Expression
1		eldifi 3473	. . 3 |- ( A e. ( _V \ _V ) -> A e. _V )
2		eldifn 3474	. . 3 |- ( A e. ( _V \ _V ) -> -. A e. _V )
3	1, 2	pm2.65i 173	. 2 |- -. A e. ( _V \ _V )
4		df-nul 3633	. . 3 |- (/) = ( _V \ _V )
5	4	eleq2i 2502	. 2 |- ( A e. (/) <-> A e. ( _V \ _V ) )
6	3, 5	mtbir 299	1 |- -. A e. (/)

Syntax hints:   -. wn 3   e. wcel 1756   _Vcvv 2967   \ cdif 3320   (/)c0 3632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-dif 3326  df-nul 3633

This theorem is referenced by:  n0i  3637  n0f  3640  rex0  3646  abvor0  3650  rab0  3653  un0  3657  in0  3658  0ss  3661  sbcel12  3670  sbcel2  3678  disj  3714  r19.2zb  3765  ral0  3779  rabsnifsb  3938  int0  4137  iun0  4221  0iun  4222  br0  4333  sbcbr123  4338  pwne0  4457  ord0eln0  4768  nlim0  4772  nsuceq0  4794  0xp  4912  csbxp  4913  dm0  5048  dm0rn0  5051  reldm0  5052  elimasni  5191  cnv0  5235  co02  5346  dffv3  5682  0fv  5718  mpt20  6151  bropopvvv  6648  tz7.44-2  6855  0we1  6938  omordi  6997  omeulem1  7013  nnmordi  7062  omabs  7078  omsmolem  7084  0er  7128  omxpenlem  7404  en3lp  7814  cantnfle  7871  cantnfleOLD  7901  r1sdom  7973  r1pwss  7983  alephordi  8236  axdc3lem2  8612  zorn2lem7  8663  brdom3  8687  canthwe  8810  nlt1pi  9067  xrinfm0  11291  elixx3g  11305  elfz2  11436  om2uzlti  11765  hashf1lem2  12201  swrd0  12319  sum0  13190  fsumsplit  13208  sumsplit  13227  fsum2dlem  13229  sadc0  13642  sadcp1  13643  saddisjlem  13652  smu01lem  13673  smu01  13674  smu02  13675  prmreclem5  13973  vdwap0  14029  ram0  14075  0catg  14617  oduclatb  15306  0g0  15426  cntzrcl  15836  pmtrfrn  15955  psgnunilem5  15991  gexdvds  16074  gsumzsplit  16409  gsumzsplitOLD  16410  dprdcntz2  16524  00lss  17000  mplcoe1  17521  mplcoe2  17524  mplcoe2OLD  17525  mplrcl  17546  strov2rcl  17667  00ply1bas  17670  dsmmbas2  18137  dsmmfi  18138  maducoeval2  18421  madugsum  18424  0ntop  18493  haust1  18931  hauspwdom  19080  kqcldsat  19281  tsmssplit  19701  ustn0  19770  0met  19916  itg11  21144  itg0  21232  bddmulibl  21291  fsumharmonic  22380  ppiublem2  22517  lgsdir2lem3  22639  nbgra0edg  23294  uvtx01vtx  23351  eupath2lem1  23549  helloworld  23609  isarchi  26150  measvuni  26580  ddemeas  26604  sibf0  26672  signstfvneq0  26925  prod0  27407  fprod2dlem  27442  opelco3  27540  wsuclem  27713  pw2f1ocnv  29339  areaquad  29545  stoweidlem34  29782  2wlkonot3v  30347  2spthonot3v  30348  clwwlknprop  30388  rusgra0edg  30526  en3lpVD  31468  bj-projval  32336