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

Theorem eq0 3470
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 3466 . . 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 1685   (/)c0 3456
This theorem is referenced by:  0el  3472  ssdif0  3514  difin0ss  3521  inssdif0  3522  ralf0  3561  disjiun  4014  0ex  4151  dm0  4891  reldm0  4895  uzwo  10277  uzwoOLD  10278  fzouzdisj  10898  hausdiag  17335  rnelfmlem  17643  nninfnub  25872  prtlem14  26153  stoweidlem34  27194  stoweidlem44  27204  bnj1476  28158
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 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
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 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-v 2791  df-dif 3156  df-nul 3457
  Copyright terms: Public domain W3C validator