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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-in 3906  df-ss 3916  df-nul 4280

This theorem is used by:  ssdifin0  4441  fvsnun1  7180  fveqf1o  7303  f1ofvswap  7307  ralxpmap  8903  difsnen  9057  domunsn  9125  limensuci  9151  pssnn  9163  marypha1lem  9403  dif1card  10013  ackbij1lem18  10238  canthp1lem1  10661  grothprim  10843  hashgval  14397  hashun3  14448  hashfun  14502  hashbclem  14517  setsfun  17263  setsfun0  17264  setsid  17299  mreexexlem4d  17735  pwssplit1  21243  islindf4  22051  selvvvval  22358  psdmul  22394  neitr  23405  regsep2  23601  restmetu  24796  volinun  25774  tdeglem4  26285  noetasuplem3  27971  noetasuplem4  27972  difeq  32993  disjdifprg  33048  tocycfvres1  33550  tocycfvres2  33551  cycpmfvlem  33552  cycpmfv3  33555  cycpmcl  33556  rprmdvdsprod  33944  evlextv  34052  measunl  34727  eulerpartlemt  34882  mthmpps  36161  cldbnd  36945  poimirlem15  38384  poimirlem16  38385  poimirlem19  38388  poimirlem27  38396  evlselvlem  43434  evlselv  43435  eldioph2lem1  43605  eldioph2lem2  43606  diophren  43654  kelac1  43904  isomenndlem  47358  seposep  49852