Theorem disjdifr 4471

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

Syntax hints:   = wceq 1542   ∖ cdif 3944   ∩ cin 3946  ∅c0 4321

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 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-clel 2811  df-rab 3434  df-v 3477  df-dif 3950  df-in 3954  df-ss 3964  df-nul 4322

This theorem is referenced by:  ssdifin0  4484  fvsnun1  7175  fveqf1o  7296  f1ofvswap  7299  ralxpmap  8886  difsnen  9049  domunsn  9123  limensuci  9149  pssnn  9164  marypha1lem  9424  dif1card  10001  ackbij1lem18  10228  canthp1lem1  10643  grothprim  10825  hashgval  14289  hashun3  14340  hashfun  14393  hashbclem  14407  setsfun  17100  setsfun0  17101  setsid  17137  mreexexlem4d  17587  pwssplit1  20658  islindf4  21377  neitr  22666  regsep2  22862  restmetu  24061  volinun  25045  tdeglem4  25559  noetasuplem3  27218  noetasuplem4  27219  difeq  31734  disjdifprg  31784  tocycfvres1  32247  tocycfvres2  32248  cycpmfvlem  32249  cycpmfv3  32252  cycpmcl  32253  measunl  33152  eulerpartlemt  33308  mthmpps  34511  cldbnd  35149  poimirlem15  36441  poimirlem16  36442  poimirlem19  36445  poimirlem27  36453  selvvvval  41107  evlselvlem  41108  evlselv  41109  eldioph2lem1  41431  eldioph2lem2  41432  diophren  41484  kelac1  41738  isomenndlem  45181  seposep  47460