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

Theorem disjdif 4073
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 3866 . 2 (𝐴𝐵) ⊆ 𝐴
2 inssdif0 3980 . 2 ((𝐴𝐵) ⊆ 𝐴 ↔ (𝐴 ∩ (𝐵𝐴)) = ∅)
31, 2mpbi 220 1 (𝐴 ∩ (𝐵𝐴)) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  cdif 3604  cin 3606  wss 3607  c0 3948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-in 3614  df-ss 3621  df-nul 3949
This theorem is referenced by:  unvdif  4075  ssdifin0  4083  difdifdir  4089  fresaun  6113  fresaunres2  6114  fvsnun1  6489  fvsnun2  6490  fveqf1o  6597  ralxpmap  7949  undifixp  7986  difsnen  8083  undom  8089  enfixsn  8110  sbthlem7  8117  sbthlem8  8118  domunsn  8151  fodomr  8152  domss2  8160  mapdom2  8172  limensuci  8177  phplem2  8181  sucdom2  8197  pssnn  8219  dif1en  8234  unfi  8268  marypha1lem  8380  brwdom2  8519  infdifsn  8592  dif1card  8871  ackbij1lem12  9091  ackbij1lem18  9097  ssfin4  9170  canthp1lem1  9512  grothprim  9694  hashgval  13160  hashinf  13162  hashfxnn0  13164  hashfOLD  13166  hashun2  13210  hashun3  13211  hashssdif  13238  hashfun  13262  hashbclem  13274  hashf1lem2  13278  fsumless  14572  cvgcmpce  14594  incexclem  14612  incexc  14613  fprodsplit1f  14765  setsfun  15940  setsfun0  15941  setsid  15961  mreexexlem3d  16353  mreexexlem4d  16354  sylow2a  18080  gsumval3a  18350  dprd2da  18487  dpjcntz  18497  dpjdisj  18498  dpjlsm  18499  dpjidcl  18503  ablfac1eu  18518  pwssplit1  19107  frlmsslss2  20162  frlmssuvc1  20181  frlmsslsp  20183  islindf4  20225  mdetdiaglem  20452  mdetrlin  20456  mdetrsca  20457  mdetralt  20462  smadiadet  20524  neitr  21032  nrmsep  21209  regsep2  21228  dfconn2  21270  fbncp  21690  filufint  21771  supnfcls  21871  flimfnfcls  21879  restmetu  22422  xrge0gsumle  22683  volinun  23360  iundisj2  23363  volsup  23370  itg2cnlem2  23574  tdeglem4  23865  amgm  24762  wilthlem2  24840  rpvmasum2  25246  axlowdimlem7  25873  axlowdimlem8  25874  axlowdimlem9  25875  axlowdimlem10  25876  axlowdimlem11  25877  axlowdimlem12  25878  difeq  29481  disjdifprg  29514  iundisj2f  29529  padct  29625  resf1o  29633  iundisj2fi  29684  fprodeq02  29697  locfinref  30036  esummono  30244  esumpad  30245  gsumesum  30249  ldgenpisyslem1  30354  measvuni  30405  measunl  30407  pmeasmono  30514  eulerpartlemt  30561  tgoldbachgtde  30866  mthmpps  31605  noextendseq  31945  noetalem2  31989  noetalem3  31990  fullfunfnv  32178  fullfunfv  32179  opnbnd  32445  cldbnd  32446  poimirlem6  33545  poimirlem7  33546  poimirlem15  33554  poimirlem16  33555  poimirlem19  33558  poimirlem22  33561  poimirlem27  33566  ismblfin  33580  diophrw  37639  eldioph2lem1  37640  eldioph2lem2  37641  diophren  37694  kelac1  37950  sumnnodd  40180  sge0ss  40947  meassle  40998  meaunle  40999  meadif  41014  meaiininclem  41021  isomenndlem  41065
  Copyright terms: Public domain W3C validator