MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difid Structured version   Visualization version   GIF version

Theorem difid 4331
Description: The difference between a class and itself is the empty set. Proposition 5.15 of [TakeutiZaring] p. 20. Also Theorem 32 of [Suppes] p. 28. (Contributed by NM, 22-Apr-2004.) (Revised by David Abernethy, 17-Jun-2012.)
Assertion
Ref Expression
difid (𝐴𝐴) = ∅

Proof of Theorem difid
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 dfdif2 3920 . 2 (𝐴𝐴) = {𝑥𝐴 ∣ ¬ 𝑥𝐴}
2 dfnul3 4287 . 2 ∅ = {𝑥𝐴 ∣ ¬ 𝑥𝐴}
31, 2eqtr4i 2764 1 (𝐴𝐴) = ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1542  wcel 2107  {crab 3406  cdif 3908  c0 4283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-rab 3407  df-dif 3914  df-nul 4284
This theorem is referenced by:  dif0  4333  difun2  4441  diftpsn3  4763  symdifid  5048  difxp1  6118  difxp2  6119  2oconcl  8450  oev2  8470  fin1a2lem13  10353  ruclem13  16129  strle1  17035  efgi1  19508  frgpuptinv  19558  gsumdifsnd  19743  dprdsn  19820  ablfac1eulem  19856  fctop  22370  cctop  22372  topcld  22402  indiscld  22458  mretopd  22459  restcld  22539  conndisj  22783  csdfil  23261  ufinffr  23296  prdsxmslem2  23901  bcth3  24711  voliunlem3  24932  sltlpss  27258  uhgr0vb  28065  uhgr0  28066  nbgr1vtx  28348  uvtx01vtx  28387  cplgr1v  28420  frgr1v  29257  1vwmgr  29262  difres  31564  imadifxp  31565  mptiffisupp  31654  difico  31733  fzodif1  31743  symgcom2  31984  cycpmrn  32041  tocyccntz  32042  lindssn  32213  lbslsat  32368  0elsiga  32770  prsiga  32787  fiunelcarsg  32973  sibf0  32991  probun  33076  ballotlemfp1  33148  onint1  34967  poimirlem22  36146  poimirlem30  36154  zrdivrng  36458  safesnsupfilb  41778  ntrk0kbimka  42399  clsk3nimkb  42400  ntrclscls00  42426  ntrclskb  42429  ntrneicls11  42450  compne  42809  fzdifsuc2  43631  dvmptfprodlem  44271  fouriercn  44559  prsal  44645  caragenuncllem  44839  carageniuncllem1  44848  caratheodorylem1  44853  gsumdifsndf  46201
  Copyright terms: Public domain W3C validator