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

Theorem eq0 3799
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 3794 . . 3  |-  ( -.  A  =  (/)  <->  E. x  x  e.  A )
2 df-ex 1618 . . 3  |-  ( E. x  x  e.  A  <->  -. 
A. x  -.  x  e.  A )
31, 2bitri 249 . 2  |-  ( -.  A  =  (/)  <->  -.  A. x  -.  x  e.  A
)
43con4bii 295 1  |-  ( A  =  (/)  <->  A. x  -.  x  e.  A )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184   A.wal 1396    = wceq 1398   E.wex 1617    e. wcel 1823   (/)c0 3783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-v 3108  df-dif 3464  df-nul 3784
This theorem is referenced by:  0el  3801  ssdif0  3873  difin0ss  3882  inssdif0  3883  ralf0  3924  disjiun  4430  0ex  4569  dm0  5205  reldm0  5209  uzwo  11145  uzwoOLD  11146  fzouzdisj  11838  hashgt0elex  12450  hausdiag  20312  rnelfmlem  20619  wzel  29620  nninfnub  30484  prtlem14  30855  stoweidlem34  32055  stoweidlem44  32065  nrhmzr  32933  zrninitoringc  33133  bnj1476  34306  bj-abfal  34875  bj-nel0  34905  bj-nul  34986  bj-nuliota  34987  bj-nuliotaALT  34988
  Copyright terms: Public domain W3C validator