Theorem disjdifr 4473

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

Syntax hints:   = wceq 1540   ∖ cdif 3948   ∩ cin 3950  ∅c0 4333

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-in 3958  df-ss 3968  df-nul 4334

This theorem is referenced by:  ssdifin0  4486  fvsnun1  7202  fveqf1o  7322  f1ofvswap  7326  ralxpmap  8936  difsnen  9093  domunsn  9167  limensuci  9193  pssnn  9208  marypha1lem  9473  dif1card  10050  ackbij1lem18  10276  canthp1lem1  10692  grothprim  10874  hashgval  14372  hashun3  14423  hashfun  14476  hashbclem  14491  setsfun  17208  setsfun0  17209  setsid  17244  mreexexlem4d  17690  pwssplit1  21058  islindf4  21858  psdmul  22170  neitr  23188  regsep2  23384  restmetu  24583  volinun  25581  tdeglem4  26099  noetasuplem3  27780  noetasuplem4  27781  difeq  32537  disjdifprg  32588  tocycfvres1  33130  tocycfvres2  33131  cycpmfvlem  33132  cycpmfv3  33135  cycpmcl  33136  rprmdvdsprod  33562  measunl  34217  eulerpartlemt  34373  mthmpps  35587  cldbnd  36327  poimirlem15  37642  poimirlem16  37643  poimirlem19  37646  poimirlem27  37654  selvvvval  42595  evlselvlem  42596  evlselv  42597  eldioph2lem1  42771  eldioph2lem2  42772  diophren  42824  kelac1  43075  isomenndlem  46545  seposep  48823