Theorem disjdifr 4425

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

Syntax hints:   = wceq 1541   ∖ cdif 3898   ∩ cin 3900  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-in 3908  df-ss 3918  df-nul 4286

This theorem is referenced by:  ssdifin0  4438  fvsnun1  7128  fveqf1o  7248  f1ofvswap  7252  ralxpmap  8834  difsnen  8987  domunsn  9055  limensuci  9081  pssnn  9093  marypha1lem  9336  dif1card  9920  ackbij1lem18  10146  canthp1lem1  10563  grothprim  10745  hashgval  14256  hashun3  14307  hashfun  14360  hashbclem  14375  setsfun  17098  setsfun0  17099  setsid  17134  mreexexlem4d  17570  pwssplit1  21011  islindf4  21793  psdmul  22109  neitr  23124  regsep2  23320  restmetu  24514  volinun  25503  tdeglem4  26021  noetasuplem3  27703  noetasuplem4  27704  difeq  32593  disjdifprg  32650  tocycfvres1  33192  tocycfvres2  33193  cycpmfvlem  33194  cycpmfv3  33197  cycpmcl  33198  rprmdvdsprod  33615  evlextv  33707  esplyind  33731  measunl  34373  eulerpartlemt  34528  mthmpps  35776  cldbnd  36520  poimirlem15  37836  poimirlem16  37837  poimirlem19  37840  poimirlem27  37848  selvvvval  42828  evlselvlem  42829  evlselv  42830  eldioph2lem1  43002  eldioph2lem2  43003  diophren  43055  kelac1  43305  isomenndlem  46774  seposep  49171