Theorem disjdifr 4427

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

Assertion

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

Proof of Theorem disjdifr

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

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3896   ∩ cin 3898  ∅c0 4279

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 2147  ax-9 2155  ax-ext 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-in 3906  df-ss 3916  df-nul 4280

This theorem is used by:  ssdifin0  4441  fvsnun1  7185  fveqf1o  7308  f1ofvswap  7312  ralxpmap  8917  difsnen  9071  domunsn  9139  limensuci  9165  pssnn  9177  marypha1lem  9418  dif1card  10082  ackbij1lem18  10307  canthp1lem1  10730  grothprim  10912  hashgval  14470  hashun3  14521  hashfun  14575  hashbclem  14590  setsfun  17342  setsfun0  17343  setsid  17378  mreexexlem4d  17814  pwssplit1  21327  islindf4  22137  selvvvval  22444  psdmul  22480  neitr  23491  regsep2  23687  restmetu  24882  volinun  25860  tdeglem4  26371  noetasuplem3  28085  noetasuplem4  28086  difeq  33107  disjdifprg  33162  tocycfvres1  33664  tocycfvres2  33665  cycpmfvlem  33666  cycpmfv3  33669  cycpmcl  33670  rprmdvdsprod  34059  evlextv  34167  measunl  34842  eulerpartlemt  34996  mthmpps  36326  cldbnd  37094  poimirlem15  38533  poimirlem16  38534  poimirlem19  38537  poimirlem27  38545  evlselvlem  43596  evlselv  43597  eldioph2lem1  43750  eldioph2lem2  43751  diophren  43799  kelac1  44049  isomenndlem  47509  seposep  50003