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

Theorem eq0 3469
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 3465 . . 3  |-  ( -.  A  =  (/)  <->  E. x  x  e.  A )
2 df-ex 1529 . . 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 1527   E.wex 1528    = wceq 1623    e. wcel 1684   (/)c0 3455
This theorem is referenced by:  0el  3471  ssdif0  3513  difin0ss  3520  inssdif0  3521  ralf0  3560  disjiun  4013  0ex  4150  dm0  4892  reldm0  4896  uzwo  10281  uzwoOLD  10282  fzouzdisj  10902  hausdiag  17339  rnelfmlem  17647  nninfnub  26461  prtlem14  26742  stoweidlem34  27783  stoweidlem44  27793  bnj1476  28879
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-nul 3456
  Copyright terms: Public domain W3C validator