Theorem disjdifr 4403

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

Syntax hints:   = wceq 1539   ∖ cdif 3880   ∩ cin 3882  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900  df-nul 4254

This theorem is referenced by:  ssdifin0  4413  fvsnun1  7036  fveqf1o  7155  f1ofvswap  7158  ralxpmap  8642  difsnen  8794  domunsn  8863  limensuci  8889  pssnn  8913  marypha1lem  9122  dif1card  9697  ackbij1lem18  9924  canthp1lem1  10339  grothprim  10521  hashgval  13975  hashun3  14027  hashfun  14080  hashbclem  14092  setsfun  16800  setsfun0  16801  setsid  16837  mreexexlem4d  17273  pwssplit1  20236  islindf4  20955  neitr  22239  regsep2  22435  restmetu  23632  volinun  24615  tdeglem4  25129  difeq  30766  disjdifprg  30815  tocycfvres1  31279  tocycfvres2  31280  cycpmfvlem  31281  cycpmfv3  31284  cycpmcl  31285  measunl  32084  eulerpartlemt  32238  mthmpps  33444  noetasuplem3  33865  noetasuplem4  33866  cldbnd  34442  poimirlem15  35719  poimirlem16  35720  poimirlem19  35723  poimirlem27  35731  eldioph2lem1  40498  eldioph2lem2  40499  diophren  40551  kelac1  40804  isomenndlem  43958  seposep  46107