Theorem disjdifr 4496

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

Syntax hints:   = wceq 1537   ∖ cdif 3973   ∩ cin 3975  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-in 3983  df-ss 3993  df-nul 4353

This theorem is referenced by:  ssdifin0  4509  fvsnun1  7216  fveqf1o  7338  f1ofvswap  7342  ralxpmap  8954  difsnen  9119  domunsn  9193  limensuci  9219  pssnn  9234  marypha1lem  9502  dif1card  10079  ackbij1lem18  10305  canthp1lem1  10721  grothprim  10903  hashgval  14382  hashun3  14433  hashfun  14486  hashbclem  14501  setsfun  17218  setsfun0  17219  setsid  17255  mreexexlem4d  17705  pwssplit1  21081  islindf4  21881  psdmul  22193  neitr  23209  regsep2  23405  restmetu  24604  volinun  25600  tdeglem4  26119  noetasuplem3  27798  noetasuplem4  27799  difeq  32548  disjdifprg  32597  tocycfvres1  33103  tocycfvres2  33104  cycpmfvlem  33105  cycpmfv3  33108  cycpmcl  33109  rprmdvdsprod  33527  measunl  34180  eulerpartlemt  34336  mthmpps  35550  cldbnd  36292  poimirlem15  37595  poimirlem16  37596  poimirlem19  37599  poimirlem27  37607  selvvvval  42540  evlselvlem  42541  evlselv  42542  eldioph2lem1  42716  eldioph2lem2  42717  diophren  42769  kelac1  43020  isomenndlem  46451  seposep  48605