Theorem disjdifr 4406

Description: A class and its relative complement are disjoint. (Contributed by Thierry Arnoux, 29-Nov-2023.)

Assertion

Ref	Expression
disjdifr	⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅

Proof of Theorem disjdifr

Step	Hyp	Ref	Expression
1		incom 4135	. 2 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ((𝐵 ∖ 𝐴) ∩ 𝐴)
2		disjdif 4405	. 2 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅
3	1, 2	eqtr3i 2768	1 ⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅

Syntax hints:   = wceq 1539   ∖ cdif 3884   ∩ cin 3886  ∅c0 4256

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904  df-nul 4257

This theorem is referenced by:  ssdifin0  4416  fvsnun1  7054  fveqf1o  7175  f1ofvswap  7178  ralxpmap  8684  difsnen  8840  domunsn  8914  limensuci  8940  pssnn  8951  marypha1lem  9192  dif1card  9766  ackbij1lem18  9993  canthp1lem1  10408  grothprim  10590  hashgval  14047  hashun3  14099  hashfun  14152  hashbclem  14164  setsfun  16872  setsfun0  16873  setsid  16909  mreexexlem4d  17356  pwssplit1  20321  islindf4  21045  neitr  22331  regsep2  22527  restmetu  23726  volinun  24710  tdeglem4  25224  difeq  30865  disjdifprg  30914  tocycfvres1  31377  tocycfvres2  31378  cycpmfvlem  31379  cycpmfv3  31382  cycpmcl  31383  measunl  32184  eulerpartlemt  32338  mthmpps  33544  noetasuplem3  33938  noetasuplem4  33939  cldbnd  34515  poimirlem15  35792  poimirlem16  35793  poimirlem19  35796  poimirlem27  35804  eldioph2lem1  40582  eldioph2lem2  40583  diophren  40635  kelac1  40888  isomenndlem  44068  seposep  46219