Theorem disjdifr 4424

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

Syntax hints:   = wceq 1559   ∖ cdif 3899   ∩ cin 3901  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-in 3909  df-ss 3919  df-nul 4284

This theorem is referenced by:  ssdifin0  4436  fvsnun1  7160  fveqf1o  7280  f1ofvswap  7284  ralxpmap  8871  difsnen  9024  domunsn  9092  limensuci  9118  pssnn  9130  marypha1lem  9372  dif1card  9959  ackbij1lem18  10185  canthp1lem1  10603  grothprim  10785  hashgval  14339  hashun3  14390  hashfun  14443  hashbclem  14458  setsfun  17197  setsfun0  17198  setsid  17233  mreexexlem4d  17669  pwssplit1  21113  islindf4  21877  selvvvval  22182  psdmul  22218  neitr  23227  regsep2  23423  restmetu  24617  volinun  25595  tdeglem4  26107  noetasuplem3  27786  noetasuplem4  27787  difeq  32676  disjdifprg  32734  tocycfvres1  33250  tocycfvres2  33251  cycpmfvlem  33252  cycpmfv3  33255  cycpmcl  33256  rprmdvdsprod  33690  evlextv  33799  esplyind  33832  measunl  34473  eulerpartlemt  34628  mthmpps  35892  cldbnd  36646  poimirlem15  38094  poimirlem16  38095  poimirlem19  38098  poimirlem27  38106  evlselvlem  43130  evlselv  43131  eldioph2lem1  43301  eldioph2lem2  43302  diophren  43350  kelac1  43600  isomenndlem  47064  seposep  49507