Theorem disjdifr 4408

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

Syntax hints:   = wceq 1547   ∖ cdif 3887   ∩ cin 3889  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-in 3897  df-ss 3907  df-nul 4269

This theorem is referenced by:  ssdifin0  4420  fvsnun1  7133  fveqf1o  7253  f1ofvswap  7257  ralxpmap  8841  difsnen  8994  domunsn  9062  limensuci  9088  pssnn  9100  marypha1lem  9343  dif1card  9930  ackbij1lem18  10156  canthp1lem1  10573  grothprim  10755  hashgval  14293  hashun3  14344  hashfun  14397  hashbclem  14412  setsfun  17139  setsfun0  17140  setsid  17175  mreexexlem4d  17611  pwssplit1  21056  islindf4  21820  selvvvval  22125  psdmul  22161  neitr  23170  regsep2  23366  restmetu  24560  volinun  25538  tdeglem4  26050  noetasuplem3  27724  noetasuplem4  27725  difeq  32613  disjdifprg  32671  tocycfvres1  33198  tocycfvres2  33199  cycpmfvlem  33200  cycpmfv3  33203  cycpmcl  33204  rprmdvdsprod  33624  evlextv  33733  esplyind  33766  measunl  34407  eulerpartlemt  34562  mthmpps  35817  cldbnd  36561  poimirlem15  38009  poimirlem16  38010  poimirlem19  38013  poimirlem27  38021  evlselvlem  43045  evlselv  43046  eldioph2lem1  43216  eldioph2lem2  43217  diophren  43265  kelac1  43515  isomenndlem  46980  seposep  49423