Theorem disjdifr 4427

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		incom 4163	. 2 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ((𝐵 ∖ 𝐴) ∩ 𝐴)
2		disjdif 4426	. 2 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅
3	1, 2	eqtr3i 2762	1 ⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅

Syntax hints:   = wceq 1542   ∖ cdif 3900   ∩ cin 3902  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-in 3910  df-ss 3920  df-nul 4288

This theorem is referenced by:  ssdifin0  4440  fvsnun1  7138  fveqf1o  7258  f1ofvswap  7262  ralxpmap  8846  difsnen  8999  domunsn  9067  limensuci  9093  pssnn  9105  marypha1lem  9348  dif1card  9932  ackbij1lem18  10158  canthp1lem1  10575  grothprim  10757  hashgval  14268  hashun3  14319  hashfun  14372  hashbclem  14387  setsfun  17110  setsfun0  17111  setsid  17146  mreexexlem4d  17582  pwssplit1  21023  islindf4  21805  psdmul  22121  neitr  23136  regsep2  23332  restmetu  24526  volinun  25515  tdeglem4  26033  noetasuplem3  27715  noetasuplem4  27716  difeq  32604  disjdifprg  32661  tocycfvres1  33203  tocycfvres2  33204  cycpmfvlem  33205  cycpmfv3  33208  cycpmcl  33209  rprmdvdsprod  33626  evlextv  33718  esplyind  33751  measunl  34393  eulerpartlemt  34548  mthmpps  35795  cldbnd  36539  poimirlem15  37883  poimirlem16  37884  poimirlem19  37887  poimirlem27  37895  selvvvval  42940  evlselvlem  42941  evlselv  42942  eldioph2lem1  43114  eldioph2lem2  43115  diophren  43167  kelac1  43417  isomenndlem  46885  seposep  49282