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 2754	1 ⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅

Syntax hints:   = wceq 1540   ∖ cdif 3902   ∩ cin 3904  ∅c0 4286

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-in 3912  df-ss 3922  df-nul 4287

This theorem is referenced by:  ssdifin0  4439  fvsnun1  7122  fveqf1o  7243  f1ofvswap  7247  ralxpmap  8830  difsnen  8983  domunsn  9051  limensuci  9077  pssnn  9092  marypha1lem  9342  dif1card  9923  ackbij1lem18  10149  canthp1lem1  10565  grothprim  10747  hashgval  14258  hashun3  14309  hashfun  14362  hashbclem  14377  setsfun  17100  setsfun0  17101  setsid  17136  mreexexlem4d  17571  pwssplit1  20981  islindf4  21763  psdmul  22069  neitr  23083  regsep2  23279  restmetu  24474  volinun  25463  tdeglem4  25981  noetasuplem3  27663  noetasuplem4  27664  difeq  32480  disjdifprg  32537  tocycfvres1  33065  tocycfvres2  33066  cycpmfvlem  33067  cycpmfv3  33070  cycpmcl  33071  rprmdvdsprod  33484  measunl  34185  eulerpartlemt  34341  mthmpps  35557  cldbnd  36302  poimirlem15  37617  poimirlem16  37618  poimirlem19  37621  poimirlem27  37629  selvvvval  42561  evlselvlem  42562  evlselv  42563  eldioph2lem1  42736  eldioph2lem2  42737  diophren  42789  kelac1  43039  isomenndlem  46515  seposep  48914