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

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

Proof of Theorem difssd
StepHypRef Expression
1 difss 3617 . 2  |-  ( A 
\  B )  C_  A
21a1i 11 1  |-  ( ph  ->  ( A  \  B
)  C_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \ cdif 3458    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-dif 3464  df-in 3468  df-ss 3475
This theorem is referenced by:  fofinf1o  7793  ackbij1lem12  8602  ssfin4  8681  enfin1ai  8755  fpwwe2  9010  wundif  9081  rpnnen2lem11  14042  mrieqvlemd  15118  mrieqv2d  15128  symgextfo  16646  symgextres  16649  symgfixelsi  16659  pmtrdifellem1  16700  pmtrdifellem2  16701  dprdfeq0  17257  dprdfeq0OLD  17264  dpjf  17301  dpjlid  17305  dpjghm  17307  ablfac1eu  17319  islbs3  17996  lbsextlem4  18002  frlmsslss2  18976  frlmsslss2OLD  18977  frlmlbs  18999  mdetrlin  19271  mdetrsca  19272  mdetralt  19277  mdetmul  19292  smadiadetlem3lem0  19334  smadiadet  19339  clsval2  19718  hausllycmp  20161  qtoprest  20384  trfil3  20555  ufileu  20586  fclscf  20692  alexsublem  20710  blcld  21174  restmetu  21256  evth  21625  lebnumlem1  21627  lebnumlem2  21628  lebnumlem3  21629  cmmbl  22111  nulmbl2  22113  volinun  22122  volsup  22132  uniioombllem3  22160  uniioombllem5  22162  uniioombl  22164  itg1addlem5  22273  itg2cnlem2  22335  dvreslem  22479  dvres2lem  22480  dvaddbr  22507  dvmulbr  22508  dvrec  22524  dvexp3  22545  dveflem  22546  dvcnvrelem2  22585  indsum  28252  esumpad  28284  esumpad2  28285  measiun  28426  difelcarsg  28518  carsgclctunlem2  28527  mthmpps  29206  dvreasin  30345  dvreacos  30346  areacirclem4  30350  iccdifprioo  31795  fprodn0f  31833  limciccioolb  31866  lptioo2  31876  lptioo1  31877  limcicciooub  31882  dvdivcncf  31963  itgvol0  32006  itgcoscmulx  32007  itgsincmulx  32012  stoweidlem28  32049  stoweidlem50  32071  dirkeritg  32123  dirkercncflem2  32125  dirkercncflem4  32127  fourierdlem39  32167  fourierdlem58  32186  fourierdlem68  32196  fourierdlem76  32204  fourierdlem102  32230  fourierdlem114  32242  fdmdifeqresdif  33185  lincdifsn  33279  lincresunit2  33333  lincresunit3lem2  33335
  Copyright terms: Public domain W3C validator