Theorem disjdif 4472

Description: A class and its relative complement are disjoint. Theorem 38 of [Suppes] p. 29. (Contributed by NM, 24-Mar-1998.)

Assertion

Ref	Expression
disjdif	⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅

Proof of Theorem disjdif

Step	Hyp	Ref	Expression
1		inss1 4229	. 2 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴
2		inssdif0 4370	. 2 ⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 ↔ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅)
3	1, 2	mpbi 229	1 ⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅

Syntax hints:   = wceq 1542   ∖ cdif 3946   ∩ cin 3948   ⊆ wss 3949  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966  df-nul 4324

This theorem is referenced by:  disjdifr  4473  unvdif  4475  difdifdir  4492  fresaun  6763  fresaunres2  6764  fvsnun2  7181  undifixp  8928  undom  9059  undomOLD  9060  enfixsn  9081  sucdom2OLD  9082  sbthlem7  9089  sbthlem8  9090  fodomr  9128  domss2  9136  mapdom2  9148  sucdom2  9206  phplem2OLD  9218  pssnnOLD  9265  dif1ennnALT  9277  unfiOLD  9313  marypha1lem  9428  brwdom2  9568  infdifsn  9652  ackbij1lem12  10226  ssfin4  10305  hashinf  14295  hashfxnn0  14297  hashun2  14343  hashun3  14344  hashssdif  14372  hashfun  14397  hashf1lem2  14417  fsumless  15742  cvgcmpce  15764  incexclem  15782  incexc  15783  fprodsplit1f  15934  mreexexlem3d  17590  sylow2a  19487  gsumval3a  19771  dprd2da  19912  dpjcntz  19922  dpjdisj  19923  dpjlsm  19924  dpjidcl  19928  ablfac1eu  19943  pwssplit1  20670  frlmsslss2  21330  frlmssuvc1  21349  mdetdiaglem  22100  mdetrlin  22104  mdetrsca  22105  mdetralt  22110  smadiadet  22172  nrmsep  22861  dfconn2  22923  fbncp  23343  filufint  23424  supnfcls  23524  flimfnfcls  23532  xrge0gsumle  24349  iundisj2  25066  volsup  25073  itg2cnlem2  25280  tdeglem4OLD  25578  amgm  26495  wilthlem2  26573  rpvmasum2  27015  noextendseq  27170  noetasuplem2  27237  noetasuplem4  27239  noetainflem2  27241  noetainflem4  27243  axlowdimlem7  28206  axlowdimlem8  28207  axlowdimlem9  28208  axlowdimlem10  28209  axlowdimlem11  28210  axlowdimlem12  28211  unidifsnne  31773  iundisj2f  31821  fressupp  31910  padct  31944  resf1o  31955  iundisj2fi  32008  fprodeq02  32029  gsummptres2  32205  cycpmconjslem2  32314  cyc3conja  32316  elrspunidl  32546  lbsdiflsp0  32711  dimkerim  32712  locfinref  32821  esummono  33052  esumpad  33053  gsumesum  33057  ldgenpisyslem1  33161  measvuni  33212  pmeasmono  33323  eulerpartlemt  33370  tgoldbachgtde  33672  satfv1lem  34353  fullfunfnv  34918  fullfunfv  34919  opnbnd  35210  pibt2  36298  poimirlem6  36494  poimirlem7  36495  poimirlem15  36503  poimirlem22  36510  ismblfin  36529  evlselv  41159  fsuppssind  41165  diophrw  41497  diophren  41551  tfsconcatfn  42088  tfsconcatfv1  42089  tfsconcatfv2  42090  sumnnodd  44346  sge0ss  45128  meassle  45179  meaunle  45180  meadif  45195  meaiininclem  45202  disjdifb  47494  seposep  47558  iscnrm3rlem1  47573