Theorem disjdifr 4430

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

Assertion

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

Proof of Theorem disjdifr

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

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 4048   ∩ cin 4092  ∅c0 4281

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-nul 4282

This theorem is used by:  ssdifin0  4444  fvsnun1  7218  fveqf1o  7341  f1ofvswap  7345  ralxpmap  8962  difsnen  9116  domunsn  9184  limensuci  9210  pssnn  9222  marypha1lem  9462  dif1card  10128  ackbij1lem18  10353  canthp1lem1  10776  grothprim  10958  hashgval  14518  hashun3  14569  hashfun  14623  hashbclem  14638  setsfun  17393  setsfun0  17394  setsid  17429  mreexexlem4d  17871  pwssplit1  21385  islindf4  22199  selvvvval  22506  psdmul  22542  neitr  23553  regsep2  23749  restmetu  24944  volinun  25922  tdeglem4  26433  noetasuplem3  28149  noetasuplem4  28150  difeq  33213  disjdifprg  33267  tocycfvres1  33770  tocycfvres2  33771  cycpmfvlem  33772  cycpmfv3  33775  cycpmcl  33776  rprmdvdsprod  34170  evlextv  34285  measunl  34960  eulerpartlemt  35114  mthmpps  36555  cldbnd  37329  poimirlem15  38821  poimirlem16  38822  poimirlem19  38825  poimirlem27  38833  evlselvlem  43882  evlselv  43883  eldioph2lem1  44037  eldioph2lem2  44038  diophren  44086  kelac1  44331  isomenndlem  47813  seposep  50371