Theorem disjdifr 4439

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

Syntax hints:   = wceq 1540   ∖ cdif 3914   ∩ cin 3916  ∅c0 4299

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-in 3924  df-ss 3934  df-nul 4300

This theorem is referenced by:  ssdifin0  4452  fvsnun1  7159  fveqf1o  7280  f1ofvswap  7284  ralxpmap  8872  difsnen  9027  domunsn  9097  limensuci  9123  pssnn  9138  marypha1lem  9391  dif1card  9970  ackbij1lem18  10196  canthp1lem1  10612  grothprim  10794  hashgval  14305  hashun3  14356  hashfun  14409  hashbclem  14424  setsfun  17148  setsfun0  17149  setsid  17184  mreexexlem4d  17615  pwssplit1  20973  islindf4  21754  psdmul  22060  neitr  23074  regsep2  23270  restmetu  24465  volinun  25454  tdeglem4  25972  noetasuplem3  27654  noetasuplem4  27655  difeq  32454  disjdifprg  32511  tocycfvres1  33074  tocycfvres2  33075  cycpmfvlem  33076  cycpmfv3  33079  cycpmcl  33080  rprmdvdsprod  33512  measunl  34213  eulerpartlemt  34369  mthmpps  35576  cldbnd  36321  poimirlem15  37636  poimirlem16  37637  poimirlem19  37640  poimirlem27  37648  selvvvval  42580  evlselvlem  42581  evlselv  42582  eldioph2lem1  42755  eldioph2lem2  42756  diophren  42808  kelac1  43059  isomenndlem  46535  seposep  48918