Theorem disjdifr 4448

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 4184	. 2 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ((𝐵 ∖ 𝐴) ∩ 𝐴)
2		disjdif 4447	. 2 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅
3	1, 2	eqtr3i 2760	1 ⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅

Syntax hints:   = wceq 1540   ∖ cdif 3923   ∩ cin 3925  ∅c0 4308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-in 3933  df-ss 3943  df-nul 4309

This theorem is referenced by:  ssdifin0  4461  fvsnun1  7174  fveqf1o  7295  f1ofvswap  7299  ralxpmap  8910  difsnen  9067  domunsn  9141  limensuci  9167  pssnn  9182  marypha1lem  9445  dif1card  10024  ackbij1lem18  10250  canthp1lem1  10666  grothprim  10848  hashgval  14351  hashun3  14402  hashfun  14455  hashbclem  14470  setsfun  17190  setsfun0  17191  setsid  17226  mreexexlem4d  17659  pwssplit1  21017  islindf4  21798  psdmul  22104  neitr  23118  regsep2  23314  restmetu  24509  volinun  25499  tdeglem4  26017  noetasuplem3  27699  noetasuplem4  27700  difeq  32499  disjdifprg  32556  tocycfvres1  33121  tocycfvres2  33122  cycpmfvlem  33123  cycpmfv3  33126  cycpmcl  33127  rprmdvdsprod  33549  measunl  34247  eulerpartlemt  34403  mthmpps  35604  cldbnd  36344  poimirlem15  37659  poimirlem16  37660  poimirlem19  37663  poimirlem27  37671  selvvvval  42608  evlselvlem  42609  evlselv  42610  eldioph2lem1  42783  eldioph2lem2  42784  diophren  42836  kelac1  43087  isomenndlem  46559  seposep  48900