Theorem disjdifr 4471

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

Syntax hints:   = wceq 1539   ∖ cdif 3944   ∩ cin 3946  ∅c0 4321

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-in 3954  df-ss 3964  df-nul 4322

This theorem is referenced by:  ssdifin0  4484  fvsnun1  7181  fveqf1o  7303  f1ofvswap  7306  ralxpmap  8892  difsnen  9055  domunsn  9129  limensuci  9155  pssnn  9170  marypha1lem  9430  dif1card  10007  ackbij1lem18  10234  canthp1lem1  10649  grothprim  10831  hashgval  14297  hashun3  14348  hashfun  14401  hashbclem  14415  setsfun  17108  setsfun0  17109  setsid  17145  mreexexlem4d  17595  pwssplit1  20814  islindf4  21612  neitr  22904  regsep2  23100  restmetu  24299  volinun  25295  tdeglem4  25812  noetasuplem3  27474  noetasuplem4  27475  difeq  32023  disjdifprg  32073  tocycfvres1  32539  tocycfvres2  32540  cycpmfvlem  32541  cycpmfv3  32544  cycpmcl  32545  measunl  33512  eulerpartlemt  33668  mthmpps  34871  cldbnd  35514  poimirlem15  36806  poimirlem16  36807  poimirlem19  36810  poimirlem27  36818  selvvvval  41459  evlselvlem  41460  evlselv  41461  eldioph2lem1  41800  eldioph2lem2  41801  diophren  41853  kelac1  42107  isomenndlem  45544  seposep  47645