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

Theorem difssd 3890
Description: A difference of two classes is contained in the minuend. Deduction form of difss 3889. (Contributed by David Moews, 1-May-2017.)
Assertion
Ref Expression
difssd (𝜑 → (𝐴𝐵) ⊆ 𝐴)

Proof of Theorem difssd
StepHypRef Expression
1 difss 3889 . 2 (𝐴𝐵) ⊆ 𝐴
21a1i 11 1 (𝜑 → (𝐴𝐵) ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  cdif 3721  wss 3724
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-dif 3727  df-in 3731  df-ss 3738
This theorem is referenced by:  uneqdifeq  4200  fofinf1o  8398  ackbij1lem12  9256  ssfin4  9335  enfin1ai  9409  fpwwe2  9668  wundif  9739  cshimadifsn  13785  fprodn0f  14929  rpnnen2lem11  15160  mrieqvlemd  16498  mrieqv2d  16508  symgextfo  18050  symgextres  18053  symgfixelsi  18063  pmtrdifellem1  18104  pmtrdifellem2  18105  dprdfeq0  18630  dpjf  18665  dpjlid  18669  dpjghm  18671  ablfac1eu  18681  islbs3  19371  lbsextlem4  19377  frlmsslss2  20332  frlmlbs  20354  mdetrlin  20627  mdetrsca  20628  mdetralt  20633  mdetmul  20648  smadiadetlem3lem0  20691  smadiadet  20696  clsval2  21076  hausllycmp  21519  qtoprest  21742  trfil3  21913  ufileu  21944  fclscf  22050  alexsublem  22069  blcld  22531  restmetu  22596  evth  22979  lebnumlem1  22981  lebnumlem2  22982  lebnumlem3  22983  cmmbl  23523  nulmbl2  23525  volinun  23535  volsup  23545  uniioombllem3  23574  uniioombllem5  23576  uniioombl  23578  itg1addlem5  23688  itg2cnlem2  23750  dvreslem  23894  dvres2lem  23895  dvaddbr  23922  dvmulbr  23923  dvrec  23939  dvexp3  23962  dveflem  23963  dvcnvrelem2  24002  uhgrspan1  26419  fprodeq02  29910  madjusmdetlem1  30234  indsum  30424  indsumin  30425  esumpad  30458  esumpad2  30459  measiun  30622  difelcarsg  30713  carsgclctunlem2  30722  tgoldbachgtde  31079  mthmpps  31818  dvreasin  33831  dvreacos  33832  areacirclem4  33836  ntrclsrcomplex  38860  clsk3nimkb  38865  ntrclsfveq1  38885  ntrclsiso  38892  ntrclsk2  38893  ntrclskb  38894  ntrclsk3  38895  ntrclsk13  38896  ntrneircomplex  38899  clsneircomplex  38928  clsneiel1  38933  neicvgrcomplex  38938  neicvgel1  38944  difmap  39918  difmapsn  39923  supminfxr2  40216  iccdifprioo  40262  limciccioolb  40372  lptioo2  40382  lptioo1  40383  limcicciooub  40388  dvdivcncf  40661  itgvol0  40702  itgcoscmulx  40703  itgsincmulx  40708  ismbl3  40721  stoweidlem28  40763  stoweidlem50  40785  dirkeritg  40837  dirkercncflem2  40839  dirkercncflem4  40841  fourierdlem39  40881  fourierdlem58  40899  fourierdlem68  40909  fourierdlem76  40917  fourierdlem102  40943  fourierdlem114  40955  pwsal  41053  salexct  41070  sge0fodjrnlem  41151  iundjiun  41195  meaunle  41199  meadjiunlem  41200  meaiunlelem  41203  meadif  41214  meaiuninclem  41215  meaiininclem  41221  carageniuncllem2  41257  caragencmpl  41270  hsphoidmvle2  41320  hsphoidmvle  41321  hoidmv1lelem2  41327  hspmbllem1  41361  hspmbllem3  41363  fdmdifeqresdif  42649  lincdifsn  42742  lincresunit2  42796  lincresunit3lem2  42798
  Copyright terms: Public domain W3C validator