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

Theorem difssd 3529
Description: A difference of two classes is contained in the minuend. Deduction form of difss 3528. (Contributed by David Moews, 1-May-2017.)
Assertion
Ref Expression
difssd  |-  ( ph  ->  ( A  \  B
)  C_  A )

Proof of Theorem difssd
StepHypRef Expression
1 difss 3528 . 2  |-  ( A 
\  B )  C_  A
21a1i 11 1  |-  ( ph  ->  ( A  \  B
)  C_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \ cdif 3369    C_ wss 3372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-v 3015  df-dif 3375  df-in 3379  df-ss 3386
This theorem is referenced by:  fofinf1o  7839  ackbij1lem12  8648  ssfin4  8727  enfin1ai  8801  fpwwe2  9055  wundif  9126  fprodn0f  14056  rpnnen2lem11  14288  mrieqvlemd  15546  mrieqv2d  15556  symgextfo  17074  symgextres  17077  symgfixelsi  17087  pmtrdifellem1  17128  pmtrdifellem2  17129  dprdfeq0  17666  dpjf  17701  dpjlid  17705  dpjghm  17707  ablfac1eu  17717  islbs3  18389  lbsextlem4  18395  frlmsslss2  19344  frlmlbs  19366  mdetrlin  19638  mdetrsca  19639  mdetralt  19644  mdetmul  19659  smadiadetlem3lem0  19701  smadiadet  19706  clsval2  20076  hausllycmp  20520  qtoprest  20743  trfil3  20914  ufileu  20945  fclscf  21051  alexsublem  21070  blcld  21531  restmetu  21596  evth  21998  lebnumlem1  22000  lebnumlem2  22001  lebnumlem3  22002  lebnumlem1OLD  22003  lebnumlem2OLD  22004  lebnumlem3OLD  22005  cmmbl  22499  nulmbl2  22501  volinun  22511  volsup  22521  uniioombllem3  22555  uniioombllem5  22557  uniioombl  22559  itg1addlem5  22670  itg2cnlem2  22732  dvreslem  22876  dvres2lem  22877  dvaddbr  22904  dvmulbr  22905  dvrec  22921  dvexp3  22942  dveflem  22943  dvcnvrelem2  22982  madjusmdetlem1  28660  indsum  28851  esumpad  28883  esumpad2  28884  measiun  29047  difelcarsg  29148  carsgclctunlem2  29157  mthmpps  30226  dvreasin  32032  dvreacos  32033  areacirclem4  32037  difmap  37499  difmapsn  37506  iccdifprioo  37658  limciccioolb  37743  lptioo2  37753  lptioo1  37754  limcicciooub  37759  dvdivcncf  37841  itgvol0  37887  itgcoscmulx  37888  itgsincmulx  37893  ismbl3  37906  stoweidlem28  37945  stoweidlem50  37968  dirkeritg  38021  dirkercncflem2  38023  dirkercncflem4  38025  fourierdlem39  38066  fourierdlem58  38085  fourierdlem68  38095  fourierdlem76  38103  fourierdlem102  38129  fourierdlem114  38141  pwsal  38233  salexct  38250  sge0fodjrnlem  38317  iundjiun  38359  meaunle  38363  meadjiunlem  38364  meaiunlelem  38367  carageniuncllem2  38407  caragencmpl  38420  hsphoidmvle2  38470  hsphoidmvle  38471  hoidmv1lelem2  38477  hspmbllem1  38511  hspmbllem3  38513  uhgrspan1  39477  fdmdifeqresdif  40448  lincdifsn  40542  lincresunit2  40596  lincresunit3lem2  40598
  Copyright terms: Public domain W3C validator