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

Theorem eq0 3471
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 3467 . . 3  |-  ( -.  A  =  (/)  <->  E. x  x  e.  A )
2 df-ex 1531 . . 3  |-  ( E. x  x  e.  A  <->  -. 
A. x  -.  x  e.  A )
31, 2bitri 240 . 2  |-  ( -.  A  =  (/)  <->  -.  A. x  -.  x  e.  A
)
43con4bii 288 1  |-  ( A  =  (/)  <->  A. x  -.  x  e.  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176   A.wal 1529   E.wex 1530    = wceq 1625    e. wcel 1686   (/)c0 3457
This theorem is referenced by:  0el  3473  ssdif0  3515  difin0ss  3522  inssdif0  3523  ralf0  3562  disjiun  4015  0ex  4152  dm0  4894  reldm0  4898  uzwo  10283  uzwoOLD  10284  fzouzdisj  10904  hausdiag  17341  rnelfmlem  17649  nninfnub  26472  prtlem14  26753  stoweidlem34  27794  stoweidlem44  27804  bnj1476  28952
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-v 2792  df-dif 3157  df-nul 3458
  Copyright terms: Public domain W3C validator