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

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

Proof of Theorem difssd
StepHypRef Expression
1 difss 3717 . 2 (𝐴𝐵) ⊆ 𝐴
21a1i 11 1 (𝜑 → (𝐴𝐵) ⊆ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  cdif 3553  wss 3556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-dif 3559  df-in 3563  df-ss 3570
This theorem is referenced by:  uneqdifeq  4031  fofinf1o  8188  ackbij1lem12  9000  ssfin4  9079  enfin1ai  9153  fpwwe2  9412  wundif  9483  cshimadifsn  13515  fprodn0f  14650  rpnnen2lem11  14881  mrieqvlemd  16213  mrieqv2d  16223  symgextfo  17766  symgextres  17769  symgfixelsi  17779  pmtrdifellem1  17820  pmtrdifellem2  17821  dprdfeq0  18345  dpjf  18380  dpjlid  18384  dpjghm  18386  ablfac1eu  18396  islbs3  19077  lbsextlem4  19083  frlmsslss2  20036  frlmlbs  20058  mdetrlin  20330  mdetrsca  20331  mdetralt  20336  mdetmul  20351  smadiadetlem3lem0  20393  smadiadet  20398  clsval2  20767  hausllycmp  21210  qtoprest  21433  trfil3  21605  ufileu  21636  fclscf  21742  alexsublem  21761  blcld  22223  restmetu  22288  evth  22671  lebnumlem1  22673  lebnumlem2  22674  lebnumlem3  22675  cmmbl  23215  nulmbl2  23217  volinun  23227  volsup  23237  uniioombllem3  23266  uniioombllem5  23268  uniioombl  23270  itg1addlem5  23380  itg2cnlem2  23442  dvreslem  23586  dvres2lem  23587  dvaddbr  23614  dvmulbr  23615  dvrec  23631  dvexp3  23652  dveflem  23653  dvcnvrelem2  23692  uhgrspan1  26095  madjusmdetlem1  29687  indsum  29878  esumpad  29910  esumpad2  29911  measiun  30074  difelcarsg  30165  carsgclctunlem2  30174  itgexpif  30463  mthmpps  31208  dvreasin  33151  dvreacos  33152  areacirclem4  33156  ntrclsrcomplex  37836  clsk3nimkb  37841  ntrclsfveq1  37861  ntrclsiso  37868  ntrclsk2  37869  ntrclskb  37870  ntrclsk3  37871  ntrclsk13  37872  ntrneircomplex  37875  clsneircomplex  37904  clsneiel1  37909  neicvgrcomplex  37914  neicvgel1  37920  difmap  38891  difmapsn  38896  iccdifprioo  39171  limciccioolb  39275  lptioo2  39285  lptioo1  39286  limcicciooub  39291  dvdivcncf  39465  itgvol0  39507  itgcoscmulx  39508  itgsincmulx  39513  ismbl3  39526  stoweidlem28  39568  stoweidlem50  39590  dirkeritg  39642  dirkercncflem2  39644  dirkercncflem4  39646  fourierdlem39  39686  fourierdlem58  39704  fourierdlem68  39714  fourierdlem76  39722  fourierdlem102  39748  fourierdlem114  39760  pwsal  39858  salexct  39875  sge0fodjrnlem  39956  iundjiun  40000  meaunle  40004  meadjiunlem  40005  meaiunlelem  40008  meadif  40019  meaiuninclem  40020  meaiininclem  40023  carageniuncllem2  40059  caragencmpl  40072  hsphoidmvle2  40122  hsphoidmvle  40123  hoidmv1lelem2  40129  hspmbllem1  40163  hspmbllem3  40165  fdmdifeqresdif  41424  lincdifsn  41517  lincresunit2  41571  lincresunit3lem2  41573
  Copyright terms: Public domain W3C validator