Theorem disjdifr 4435

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

Assertion

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

Proof of Theorem disjdifr

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

Syntax hints:   = wceq 1570   ∖ cdif 3903   ∩ cin 3905  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-in 3913  df-ss 3923  df-nul 4288

This theorem is referenced by:  ssdifin0  4447  fvsnun1  7182  fveqf1o  7302  f1ofvswap  7306  ralxpmap  8895  difsnen  9048  domunsn  9116  limensuci  9142  pssnn  9154  marypha1lem  9394  dif1card  9995  ackbij1lem18  10220  canthp1lem1  10638  grothprim  10820  hashgval  14371  hashun3  14422  hashfun  14476  hashbclem  14491  setsfun  17232  setsfun0  17233  setsid  17268  mreexexlem4d  17704  pwssplit1  21161  islindf4  21969  selvvvval  22274  psdmul  22310  neitr  23318  regsep2  23514  restmetu  24708  volinun  25686  tdeglem4  26198  noetasuplem3  27880  noetasuplem4  27881  difeq  32845  disjdifprg  32901  tocycfvres1  33411  tocycfvres2  33412  cycpmfvlem  33413  cycpmfv3  33416  cycpmcl  33417  rprmdvdsprod  33805  evlextv  33913  measunl  34587  eulerpartlemt  34742  mthmpps  36055  cldbnd  36818  poimirlem15  38267  poimirlem16  38268  poimirlem19  38271  poimirlem27  38279  evlselvlem  43303  evlselv  43304  eldioph2lem1  43474  eldioph2lem2  43475  diophren  43523  kelac1  43773  isomenndlem  47227  seposep  49687