MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eq0 Structured version   Visualization version   Unicode version

Theorem eq0 3758
Description: The empty set has no elements. Theorem 2 of [Suppes] p. 22. (Contributed by NM, 29-Aug-1993.)
Assertion
Ref Expression
eq0  |-  ( A  =  (/)  <->  A. x  -.  x  e.  A )
Distinct variable group:    x, A

Proof of Theorem eq0
StepHypRef Expression
1 neq0 3753 . . 3  |-  ( -.  A  =  (/)  <->  E. x  x  e.  A )
2 df-ex 1674 . . 3  |-  ( E. x  x  e.  A  <->  -. 
A. x  -.  x  e.  A )
31, 2bitri 257 . 2  |-  ( -.  A  =  (/)  <->  -.  A. x  -.  x  e.  A
)
43con4bii 303 1  |-  ( A  =  (/)  <->  A. x  -.  x  e.  A )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 189   A.wal 1452    = wceq 1454   E.wex 1673    e. wcel 1897   (/)c0 3742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-v 3058  df-dif 3418  df-nul 3743
This theorem is referenced by:  0el  3760  ssdif0  3834  difin0ss  3844  inssdif0  3845  ralf0  3887  disjiun  4406  0ex  4548  dm0  5066  reldm0  5070  uzwo  11250  fzouzdisj  11984  hashgt0elex  12609  hausdiag  20708  rnelfmlem  21015  bnj1476  29706  wzel  30555  bj-abfal  31553  bj-nel0  31585  bj-nul  31666  bj-nuliota  31667  bj-nuliotaALT  31668  nninfnub  32124  prtlem14  32490  stoweidlem34  37932  stoweidlem44  37942  nrhmzr  40145  zrninitoringc  40345
  Copyright terms: Public domain W3C validator