MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  disjdif Structured version   Visualization version   GIF version

Theorem disjdif 4424
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
StepHypRef Expression
1 inss1 4209 . 2 (𝐴𝐵) ⊆ 𝐴
2 inssdif0 4333 . 2 ((𝐴𝐵) ⊆ 𝐴 ↔ (𝐴 ∩ (𝐵𝐴)) = ∅)
31, 2mpbi 231 1 (𝐴 ∩ (𝐵𝐴)) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  cdif 3937  cin 3939  wss 3940  c0 4295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-dif 3943  df-in 3947  df-ss 3956  df-nul 4296
This theorem is referenced by:  unvdif  4426  ssdifin0  4434  difdifdir  4440  fresaun  6548  fresaunres2  6549  fvsnun1  6942  fvsnun2  6943  fveqf1o  7054  ralxpmap  8454  undifixp  8492  difsnen  8593  undom  8599  enfixsn  8620  sbthlem7  8627  sbthlem8  8628  domunsn  8661  fodomr  8662  domss2  8670  mapdom2  8682  limensuci  8687  phplem2  8691  sucdom2  8708  pssnn  8730  dif1en  8745  unfi  8779  marypha1lem  8891  brwdom2  9031  infdifsn  9114  dif1card  9430  ackbij1lem12  9647  ackbij1lem18  9653  ssfin4  9726  canthp1lem1  10068  grothprim  10250  hashgval  13688  hashinf  13690  hashfxnn0  13692  hashun2  13739  hashun3  13740  hashssdif  13768  hashfun  13793  hashbclem  13805  hashf1lem2  13809  fsumless  15146  cvgcmpce  15168  incexclem  15186  incexc  15187  fprodsplit1f  15339  setsfun  16513  setsfun0  16514  setsid  16533  mreexexlem3d  16912  mreexexlem4d  16913  sylow2a  18680  gsumval3a  18959  dprd2da  19100  dpjcntz  19110  dpjdisj  19111  dpjlsm  19112  dpjidcl  19116  ablfac1eu  19131  pwssplit1  19767  frlmsslss2  20854  frlmssuvc1  20873  frlmsslsp  20875  islindf4  20917  mdetdiaglem  21142  mdetrlin  21146  mdetrsca  21147  mdetralt  21152  smadiadet  21214  neitr  21723  nrmsep  21900  regsep2  21919  dfconn2  21962  fbncp  22382  filufint  22463  supnfcls  22563  flimfnfcls  22571  restmetu  23114  xrge0gsumle  23375  volinun  24081  iundisj2  24084  volsup  24091  itg2cnlem2  24297  tdeglem4  24588  amgm  25501  wilthlem2  25579  rpvmasum2  26021  axlowdimlem7  26667  axlowdimlem8  26668  axlowdimlem9  26669  axlowdimlem10  26670  axlowdimlem11  26671  axlowdimlem12  26672  disjdifr  30208  difeq  30213  unidifsnne  30229  disjdifprg  30259  iundisj2f  30274  padct  30387  resf1o  30398  iundisj2fi  30452  fprodeq02  30472  tocycfvres1  30685  tocycfvres2  30686  cycpmfvlem  30687  cycpmfv3  30690  cycpmcl  30691  cycpmconjslem2  30730  cyc3conja  30732  lbsdiflsp0  30927  dimkerim  30928  locfinref  31010  esummono  31218  esumpad  31219  gsumesum  31223  ldgenpisyslem1  31327  measvuni  31378  measunl  31380  pmeasmono  31487  eulerpartlemt  31534  tgoldbachgtde  31836  satfv1lem  32512  mthmpps  32732  noextendseq  33077  noetalem2  33121  noetalem3  33122  fullfunfnv  33310  fullfunfv  33311  opnbnd  33576  cldbnd  33577  pibt2  34586  poimirlem6  34784  poimirlem7  34785  poimirlem15  34793  poimirlem16  34794  poimirlem19  34797  poimirlem22  34800  poimirlem27  34805  ismblfin  34819  diophrw  39240  eldioph2lem1  39241  eldioph2lem2  39242  diophren  39294  kelac1  39547  sumnnodd  41795  sge0ss  42579  meassle  42630  meaunle  42631  meadif  42646  meaiininclem  42653  isomenndlem  42697
  Copyright terms: Public domain W3C validator