Theorem disjdifr 4413

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 4412	. 2 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅
2	1	ineqcomi 4151	1 ⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅

Syntax hints:   = wceq 1542   ∖ cdif 3886   ∩ cin 3888  ∅c0 4273

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-in 3896  df-ss 3906  df-nul 4274

This theorem is referenced by:  ssdifin0  4425  fvsnun1  7137  fveqf1o  7257  f1ofvswap  7261  ralxpmap  8844  difsnen  8997  domunsn  9065  limensuci  9091  pssnn  9103  marypha1lem  9346  dif1card  9932  ackbij1lem18  10158  canthp1lem1  10575  grothprim  10757  hashgval  14295  hashun3  14346  hashfun  14399  hashbclem  14414  setsfun  17141  setsfun0  17142  setsid  17177  mreexexlem4d  17613  pwssplit1  21054  islindf4  21818  psdmul  22132  neitr  23145  regsep2  23341  restmetu  24535  volinun  25513  tdeglem4  26025  noetasuplem3  27699  noetasuplem4  27700  difeq  32588  disjdifprg  32645  tocycfvres1  33171  tocycfvres2  33172  cycpmfvlem  33173  cycpmfv3  33176  cycpmcl  33177  rprmdvdsprod  33594  evlextv  33686  esplyind  33719  measunl  34360  eulerpartlemt  34515  mthmpps  35764  cldbnd  36508  poimirlem15  37956  poimirlem16  37957  poimirlem19  37960  poimirlem27  37968  selvvvval  43018  evlselvlem  43019  evlselv  43020  eldioph2lem1  43192  eldioph2lem2  43193  diophren  43241  kelac1  43491  isomenndlem  46958  seposep  49401