Theorem disjdifr 4436

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

Syntax hints:   = wceq 1540   ∖ cdif 3911   ∩ cin 3913  ∅c0 4296

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 3406  df-v 3449  df-dif 3917  df-in 3921  df-ss 3931  df-nul 4297

This theorem is referenced by:  ssdifin0  4449  fvsnun1  7156  fveqf1o  7277  f1ofvswap  7281  ralxpmap  8869  difsnen  9023  domunsn  9091  limensuci  9117  pssnn  9132  marypha1lem  9384  dif1card  9963  ackbij1lem18  10189  canthp1lem1  10605  grothprim  10787  hashgval  14298  hashun3  14349  hashfun  14402  hashbclem  14417  setsfun  17141  setsfun0  17142  setsid  17177  mreexexlem4d  17608  pwssplit1  20966  islindf4  21747  psdmul  22053  neitr  23067  regsep2  23263  restmetu  24458  volinun  25447  tdeglem4  25965  noetasuplem3  27647  noetasuplem4  27648  difeq  32447  disjdifprg  32504  tocycfvres1  33067  tocycfvres2  33068  cycpmfvlem  33069  cycpmfv3  33072  cycpmcl  33073  rprmdvdsprod  33505  measunl  34206  eulerpartlemt  34362  mthmpps  35569  cldbnd  36314  poimirlem15  37629  poimirlem16  37630  poimirlem19  37633  poimirlem27  37641  selvvvval  42573  evlselvlem  42574  evlselv  42575  eldioph2lem1  42748  eldioph2lem2  42749  diophren  42801  kelac1  43052  isomenndlem  46528  seposep  48914