Theorem disjdifr 4422

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

Syntax hints:   = wceq 1541   ∖ cdif 3895   ∩ cin 3897  ∅c0 4282

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-in 3905  df-ss 3915  df-nul 4283

This theorem is referenced by:  ssdifin0  4435  fvsnun1  7124  fveqf1o  7244  f1ofvswap  7248  ralxpmap  8828  difsnen  8981  domunsn  9049  limensuci  9075  pssnn  9087  marypha1lem  9326  dif1card  9910  ackbij1lem18  10136  canthp1lem1  10552  grothprim  10734  hashgval  14244  hashun3  14295  hashfun  14348  hashbclem  14363  setsfun  17086  setsfun0  17087  setsid  17122  mreexexlem4d  17557  pwssplit1  20997  islindf4  21779  psdmul  22084  neitr  23098  regsep2  23294  restmetu  24488  volinun  25477  tdeglem4  25995  noetasuplem3  27677  noetasuplem4  27678  difeq  32502  disjdifprg  32559  tocycfvres1  33088  tocycfvres2  33089  cycpmfvlem  33090  cycpmfv3  33093  cycpmcl  33094  rprmdvdsprod  33508  esplyind  33615  measunl  34252  eulerpartlemt  34407  mthmpps  35649  cldbnd  36393  poimirlem15  37698  poimirlem16  37699  poimirlem19  37702  poimirlem27  37710  selvvvval  42706  evlselvlem  42707  evlselv  42708  eldioph2lem1  42880  eldioph2lem2  42881  diophren  42933  kelac1  43183  isomenndlem  46655  seposep  49053