Theorem disjdifr 4426

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

Syntax hints:   = wceq 1542   ∖ cdif 3899   ∩ cin 3901  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3401  df-v 3443  df-dif 3905  df-in 3909  df-ss 3919  df-nul 4287

This theorem is referenced by:  ssdifin0  4439  fvsnun1  7130  fveqf1o  7250  f1ofvswap  7254  ralxpmap  8838  difsnen  8991  domunsn  9059  limensuci  9085  pssnn  9097  marypha1lem  9340  dif1card  9924  ackbij1lem18  10150  canthp1lem1  10567  grothprim  10749  hashgval  14260  hashun3  14311  hashfun  14364  hashbclem  14379  setsfun  17102  setsfun0  17103  setsid  17138  mreexexlem4d  17574  pwssplit1  21015  islindf4  21797  psdmul  22113  neitr  23128  regsep2  23324  restmetu  24518  volinun  25507  tdeglem4  26025  noetasuplem3  27707  noetasuplem4  27708  difeq  32575  disjdifprg  32632  tocycfvres1  33173  tocycfvres2  33174  cycpmfvlem  33175  cycpmfv3  33178  cycpmcl  33179  rprmdvdsprod  33596  evlextv  33688  esplyind  33712  measunl  34354  eulerpartlemt  34509  mthmpps  35757  cldbnd  36501  poimirlem15  37807  poimirlem16  37808  poimirlem19  37811  poimirlem27  37819  selvvvval  42864  evlselvlem  42865  evlselv  42866  eldioph2lem1  43038  eldioph2lem2  43039  diophren  43091  kelac1  43341  isomenndlem  46810  seposep  49207