Theorem disjdifr 4414

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		disjdif 4413	. 2 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅
2	1	ineqcomi 4152	1 ⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅

Syntax hints:   = wceq 1542   ∖ cdif 3887   ∩ cin 3889  ∅c0 4274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-in 3897  df-ss 3907  df-nul 4275

This theorem is referenced by:  ssdifin0  4426  fvsnun1  7130  fveqf1o  7250  f1ofvswap  7254  ralxpmap  8837  difsnen  8990  domunsn  9058  limensuci  9084  pssnn  9096  marypha1lem  9339  dif1card  9923  ackbij1lem18  10149  canthp1lem1  10566  grothprim  10748  hashgval  14286  hashun3  14337  hashfun  14390  hashbclem  14405  setsfun  17132  setsfun0  17133  setsid  17168  mreexexlem4d  17604  pwssplit1  21046  islindf4  21828  psdmul  22142  neitr  23155  regsep2  23351  restmetu  24545  volinun  25523  tdeglem4  26035  noetasuplem3  27713  noetasuplem4  27714  difeq  32603  disjdifprg  32660  tocycfvres1  33186  tocycfvres2  33187  cycpmfvlem  33188  cycpmfv3  33191  cycpmcl  33192  rprmdvdsprod  33609  evlextv  33701  esplyind  33734  measunl  34376  eulerpartlemt  34531  mthmpps  35780  cldbnd  36524  poimirlem15  37970  poimirlem16  37971  poimirlem19  37974  poimirlem27  37982  selvvvval  43032  evlselvlem  43033  evlselv  43034  eldioph2lem1  43206  eldioph2lem2  43207  diophren  43259  kelac1  43509  isomenndlem  46976  seposep  49413