Theorem disjdifr 4479

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

Syntax hints:   = wceq 1537   ∖ cdif 3960   ∩ cin 3962  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-in 3970  df-ss 3980  df-nul 4340

This theorem is referenced by:  ssdifin0  4492  fvsnun1  7202  fveqf1o  7322  f1ofvswap  7326  ralxpmap  8935  difsnen  9092  domunsn  9166  limensuci  9192  pssnn  9207  marypha1lem  9471  dif1card  10048  ackbij1lem18  10274  canthp1lem1  10690  grothprim  10872  hashgval  14369  hashun3  14420  hashfun  14473  hashbclem  14488  setsfun  17205  setsfun0  17206  setsid  17242  mreexexlem4d  17692  pwssplit1  21076  islindf4  21876  psdmul  22188  neitr  23204  regsep2  23400  restmetu  24599  volinun  25595  tdeglem4  26114  noetasuplem3  27795  noetasuplem4  27796  difeq  32546  disjdifprg  32595  tocycfvres1  33113  tocycfvres2  33114  cycpmfvlem  33115  cycpmfv3  33118  cycpmcl  33119  rprmdvdsprod  33542  measunl  34197  eulerpartlemt  34353  mthmpps  35567  cldbnd  36309  poimirlem15  37622  poimirlem16  37623  poimirlem19  37626  poimirlem27  37634  selvvvval  42572  evlselvlem  42573  evlselv  42574  eldioph2lem1  42748  eldioph2lem2  42749  diophren  42801  kelac1  43052  isomenndlem  46486  seposep  48722