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

Theorem disjdif 4031
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 3825 . 2 (𝐴𝐵) ⊆ 𝐴
2 inssdif0 3938 . 2 ((𝐴𝐵) ⊆ 𝐴 ↔ (𝐴 ∩ (𝐵𝐴)) = ∅)
31, 2mpbi 220 1 (𝐴 ∩ (𝐵𝐴)) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1481  cdif 3564  cin 3566  wss 3567  c0 3907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-dif 3570  df-in 3574  df-ss 3581  df-nul 3908
This theorem is referenced by:  unvdif  4033  ssdifin0  4041  difdifdir  4047  fresaun  6062  fresaunres2  6063  fvsnun1  6433  fvsnun2  6434  fveqf1o  6542  ralxpmap  7892  undifixp  7929  difsnen  8027  undom  8033  enfixsn  8054  sbthlem7  8061  sbthlem8  8062  domunsn  8095  fodomr  8096  domss2  8104  mapdom2  8116  limensuci  8121  phplem2  8125  sucdom2  8141  pssnn  8163  dif1en  8178  unfi  8212  marypha1lem  8324  brwdom2  8463  infdifsn  8539  dif1card  8818  ackbij1lem12  9038  ackbij1lem18  9044  ssfin4  9117  canthp1lem1  9459  grothprim  9641  hashgval  13103  hashinf  13105  hashfxnn0  13107  hashfOLD  13109  hashun2  13155  hashun3  13156  hashssdif  13183  hashfun  13207  hashbclem  13219  hashf1lem2  13223  fsumless  14509  cvgcmpce  14531  incexclem  14549  incexc  14550  fprodsplit1f  14702  setsfun  15874  setsfun0  15875  setsid  15895  mreexexlem3d  16287  mreexexlem4d  16288  sylow2a  18015  gsumval3a  18285  dprd2da  18422  dpjcntz  18432  dpjdisj  18433  dpjlsm  18434  dpjidcl  18438  ablfac1eu  18453  pwssplit1  19040  frlmsslss2  20095  frlmssuvc1  20114  frlmsslsp  20116  islindf4  20158  mdetdiaglem  20385  mdetrlin  20389  mdetrsca  20390  mdetralt  20395  smadiadet  20457  neitr  20965  nrmsep  21142  regsep2  21161  dfconn2  21203  fbncp  21624  filufint  21705  supnfcls  21805  flimfnfcls  21813  restmetu  22356  xrge0gsumle  22617  volinun  23295  iundisj2  23298  volsup  23305  itg2cnlem2  23510  tdeglem4  23801  amgm  24698  wilthlem2  24776  rpvmasum2  25182  axlowdimlem7  25809  axlowdimlem8  25810  axlowdimlem9  25811  axlowdimlem10  25812  axlowdimlem11  25813  axlowdimlem12  25814  difeq  29327  disjdifprg  29360  iundisj2f  29375  padct  29471  resf1o  29479  iundisj2fi  29530  fprodeq02  29543  locfinref  29882  esummono  30090  esumpad  30091  gsumesum  30095  ldgenpisyslem1  30200  measvuni  30251  measunl  30253  pmeasmono  30360  eulerpartlemt  30407  tgoldbachgtde  30712  mthmpps  31453  noextendseq  31794  noetalem2  31838  noetalem3  31839  fullfunfnv  32028  fullfunfv  32029  opnbnd  32295  cldbnd  32296  poimirlem6  33386  poimirlem7  33387  poimirlem15  33395  poimirlem16  33396  poimirlem19  33399  poimirlem22  33402  poimirlem27  33407  ismblfin  33421  diophrw  37141  eldioph2lem1  37142  eldioph2lem2  37143  diophren  37196  kelac1  37452  sumnnodd  39662  sge0ss  40392  meassle  40443  meaunle  40444  meadif  40459  meaiininclem  40463  isomenndlem  40507
  Copyright terms: Public domain W3C validator