Theorem disjdifr 4430

Description: A class and its relative complement are disjoint. (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 4166	1 ⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅

Syntax hints:   = wceq 1563   ∖ cdif 3904   ∩ cin 3906  ∅c0 4288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-in 3914  df-ss 3924  df-nul 4289

This theorem is referenced by:  ssdifin0  4442  fvsnun1  7170  fveqf1o  7290  f1ofvswap  7294  ralxpmap  8882  difsnen  9035  domunsn  9103  limensuci  9129  pssnn  9141  marypha1lem  9381  dif1card  9982  ackbij1lem18  10207  canthp1lem1  10625  grothprim  10807  hashgval  14357  hashun3  14408  hashfun  14462  hashbclem  14477  setsfun  17219  setsfun0  17220  setsid  17255  mreexexlem4d  17691  pwssplit1  21146  islindf4  21945  selvvvval  22250  psdmul  22286  neitr  23294  regsep2  23490  restmetu  24684  volinun  25662  tdeglem4  26174  noetasuplem3  27853  noetasuplem4  27854  difeq  32770  disjdifprg  32826  tocycfvres1  33338  tocycfvres2  33339  cycpmfvlem  33340  cycpmfv3  33343  cycpmcl  33344  rprmdvdsprod  33736  evlextv  33844  measunl  34518  eulerpartlemt  34673  mthmpps  35940  cldbnd  36694  poimirlem15  38141  poimirlem16  38142  poimirlem19  38145  poimirlem27  38153  evlselvlem  43177  evlselv  43178  eldioph2lem1  43348  eldioph2lem2  43349  diophren  43397  kelac1  43647  isomenndlem  47103  seposep  49556