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

Theorem disjdifr 4437
Description: A class and its relative complement are disjoint. (Contributed by Thierry Arnoux, 29-Nov-2023.)
Assertion
Ref Expression
disjdifr ((𝐵𝐴) ∩ 𝐴) = ∅

Proof of Theorem disjdifr
StepHypRef Expression
1 incom 4166 . 2 (𝐴 ∩ (𝐵𝐴)) = ((𝐵𝐴) ∩ 𝐴)
2 disjdif 4436 . 2 (𝐴 ∩ (𝐵𝐴)) = ∅
31, 2eqtr3i 2767 1 ((𝐵𝐴) ∩ 𝐴) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cdif 3912  cin 3914  c0 4287
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-8 2109  ax-9 2117  ax-ext 2708
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 2715  df-cleq 2729  df-clel 2815  df-rab 3411  df-v 3450  df-dif 3918  df-in 3922  df-ss 3932  df-nul 4288
This theorem is referenced by:  ssdifin0  4448  fvsnun1  7133  fveqf1o  7254  f1ofvswap  7257  ralxpmap  8841  difsnen  9004  domunsn  9078  limensuci  9104  pssnn  9119  marypha1lem  9376  dif1card  9953  ackbij1lem18  10180  canthp1lem1  10595  grothprim  10777  hashgval  14240  hashun3  14291  hashfun  14344  hashbclem  14356  setsfun  17050  setsfun0  17051  setsid  17087  mreexexlem4d  17534  pwssplit1  20536  islindf4  21260  neitr  22547  regsep2  22743  restmetu  23942  volinun  24926  tdeglem4  25440  noetasuplem3  27099  noetasuplem4  27100  difeq  31487  disjdifprg  31535  tocycfvres1  32001  tocycfvres2  32002  cycpmfvlem  32003  cycpmfv3  32006  cycpmcl  32007  measunl  32855  eulerpartlemt  33011  mthmpps  34216  cldbnd  34827  poimirlem15  36122  poimirlem16  36123  poimirlem19  36126  poimirlem27  36134  eldioph2lem1  41112  eldioph2lem2  41113  diophren  41165  kelac1  41419  isomenndlem  44845  seposep  47032
  Copyright terms: Public domain W3C validator