Theorem disjdifr 4434

Description: A class and its relative complement are disjoint. Commuted form of disjdif 4433. (Contributed by Thierry Arnoux, 29-Nov-2023.)

Assertion

Ref	Expression
disjdifr	⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅

Proof of Theorem disjdifr

Step	Hyp	Ref	Expression
1		disjdif 4433	. 2 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅
2	1	ineqcomi 4164	1 ⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3903   ∩ cin 3905  ∅c0 4286

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-in 3913  df-ss 3923  df-nul 4287

This theorem is used by:  ssdifin0  4448  fvsnun1  7184  fveqf1o  7306  f1ofvswap  7310  ralxpmap  8896  difsnen  9050  domunsn  9118  limensuci  9144  pssnn  9156  marypha1lem  9396  dif1card  10006  ackbij1lem18  10231  canthp1lem1  10648  grothprim  10830  hashgval  14382  hashun3  14433  hashfun  14487  hashbclem  14502  setsfun  17248  setsfun0  17249  setsid  17284  mreexexlem4d  17720  pwssplit1  21209  islindf4  22017  selvvvval  22322  psdmul  22358  neitr  23366  regsep2  23562  restmetu  24756  volinun  25734  tdeglem4  26246  noetasuplem3  27928  noetasuplem4  27929  difeq  32893  disjdifprg  32949  tocycfvres1  33453  tocycfvres2  33454  cycpmfvlem  33455  cycpmfv3  33458  cycpmcl  33459  rprmdvdsprod  33847  evlextv  33955  measunl  34630  eulerpartlemt  34785  mthmpps  36087  cldbnd  36870  poimirlem15  38319  poimirlem16  38320  poimirlem19  38323  poimirlem27  38331  evlselvlem  43353  evlselv  43354  eldioph2lem1  43524  eldioph2lem2  43525  diophren  43573  kelac1  43823  isomenndlem  47277  seposep  49737