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

Theorem eq0 3545
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 3541 . . 3  |-  ( -.  A  =  (/)  <->  E. x  x  e.  A )
2 df-ex 1542 . . 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 1540   E.wex 1541    = wceq 1642    e. wcel 1710   (/)c0 3531
This theorem is referenced by:  0el  3547  ssdif0  3589  difin0ss  3596  inssdif0  3597  ralf0  3636  disjiun  4094  0ex  4231  dm0  4974  reldm0  4978  uzwo  10373  uzwoOLD  10374  fzouzdisj  10994  hausdiag  17445  rnelfmlem  17749  nninfnub  25785  prtlem14  26065  stoweidlem34  27106  stoweidlem44  27116  hashgt0elex  27491  bnj1476  28641
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-v 2866  df-dif 3231  df-nul 3532
  Copyright terms: Public domain W3C validator