Theorem disjdifr 4423

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

Syntax hints:   = wceq 1541   ∖ cdif 3899   ∩ cin 3901  ∅c0 4283

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-in 3909  df-ss 3919  df-nul 4284

This theorem is referenced by:  ssdifin0  4436  fvsnun1  7116  fveqf1o  7236  f1ofvswap  7240  ralxpmap  8820  difsnen  8972  domunsn  9040  limensuci  9066  pssnn  9078  marypha1lem  9317  dif1card  9901  ackbij1lem18  10127  canthp1lem1  10543  grothprim  10725  hashgval  14240  hashun3  14291  hashfun  14344  hashbclem  14359  setsfun  17082  setsfun0  17083  setsid  17118  mreexexlem4d  17553  pwssplit1  20994  islindf4  21776  psdmul  22082  neitr  23096  regsep2  23292  restmetu  24486  volinun  25475  tdeglem4  25993  noetasuplem3  27675  noetasuplem4  27676  difeq  32496  disjdifprg  32553  tocycfvres1  33077  tocycfvres2  33078  cycpmfvlem  33079  cycpmfv3  33082  cycpmcl  33083  rprmdvdsprod  33497  measunl  34227  eulerpartlemt  34382  mthmpps  35624  cldbnd  36366  poimirlem15  37681  poimirlem16  37682  poimirlem19  37685  poimirlem27  37693  selvvvval  42624  evlselvlem  42625  evlselv  42626  eldioph2lem1  42799  eldioph2lem2  42800  diophren  42852  kelac1  43102  isomenndlem  46574  seposep  48963