Theorem disjdifr 4426

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

Assertion

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

Proof of Theorem disjdifr

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

This proof depends on syntax axioms:   = wceq 1569   ∖ cdif 4045   ∩ cin 4089  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-nul 4279

This theorem is used by:  ssdifin0  4440  fvsnun1  7188  fveqf1o  7311  f1ofvswap  7315  ralxpmap  8928  difsnen  9082  domunsn  9150  limensuci  9176  pssnn  9188  marypha1lem  9429  dif1card  10093  ackbij1lem18  10318  canthp1lem1  10741  grothprim  10923  hashgval  14481  hashun3  14532  hashfun  14586  hashbclem  14601  setsfun  17355  setsfun0  17356  setsid  17391  mreexexlem4d  17827  pwssplit1  21340  islindf4  22150  selvvvval  22457  psdmul  22493  neitr  23504  regsep2  23700  restmetu  24895  volinun  25873  tdeglem4  26384  noetasuplem3  28098  noetasuplem4  28099  difeq  33162  disjdifprg  33217  tocycfvres1  33718  tocycfvres2  33719  cycpmfvlem  33720  cycpmfv3  33723  cycpmcl  33724  rprmdvdsprod  34113  evlextv  34221  measunl  34896  eulerpartlemt  35050  mthmpps  36434  cldbnd  37207  poimirlem15  38647  poimirlem16  38648  poimirlem19  38651  poimirlem27  38659  evlselvlem  43710  evlselv  43711  eldioph2lem1  43865  eldioph2lem2  43866  diophren  43914  kelac1  44159  isomenndlem  47634  seposep  50134