Theorem disjdifr 4439

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

Syntax hints:   = wceq 1567   ∖ cdif 3910   ∩ cin 3912  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-in 3920  df-ss 3930  df-nul 4295

This theorem is referenced by:  ssdifin0  4451  fvsnun1  7181  fveqf1o  7301  f1ofvswap  7305  ralxpmap  8894  difsnen  9047  domunsn  9115  limensuci  9141  pssnn  9153  marypha1lem  9393  dif1card  9994  ackbij1lem18  10219  canthp1lem1  10637  grothprim  10819  hashgval  14369  hashun3  14420  hashfun  14474  hashbclem  14489  setsfun  17231  setsfun0  17232  setsid  17267  mreexexlem4d  17703  pwssplit1  21158  islindf4  21957  selvvvval  22262  psdmul  22298  neitr  23306  regsep2  23502  restmetu  24696  volinun  25674  tdeglem4  26186  noetasuplem3  27865  noetasuplem4  27866  difeq  32805  disjdifprg  32861  tocycfvres1  33371  tocycfvres2  33372  cycpmfvlem  33373  cycpmfv3  33376  cycpmcl  33377  rprmdvdsprod  33769  evlextv  33877  measunl  34551  eulerpartlemt  34706  mthmpps  35973  cldbnd  36726  poimirlem15  38174  poimirlem16  38175  poimirlem19  38178  poimirlem27  38186  evlselvlem  43212  evlselv  43213  eldioph2lem1  43383  eldioph2lem2  43384  diophren  43432  kelac1  43682  isomenndlem  47136  seposep  49589