Theorem difssd 3738

Description: A difference of two classes is contained in the minuend. Deduction form of difss 3737. (Contributed by David Moews, 1-May-2017.)

Assertion

Ref	Expression
difssd	|- ( ph -> ( A \ B ) C_ A )

Proof of Theorem difssd

Step	Hyp	Ref	Expression
1		difss 3737	. 2 |- ( A \ B ) C_ A
2	1	a1i 11	1 |- ( ph -> ( A \ B ) C_ A )

Syntax hints:   -> wi 4   \ cdif 3571   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588

This theorem is referenced by:  uneqdifeq  4057  fofinf1o  8241  ackbij1lem12  9053  ssfin4  9132  enfin1ai  9206  fpwwe2  9465  wundif  9536  cshimadifsn  13575  fprodn0f  14722  rpnnen2lem11  14953  mrieqvlemd  16289  mrieqv2d  16299  symgextfo  17842  symgextres  17845  symgfixelsi  17855  pmtrdifellem1  17896  pmtrdifellem2  17897  dprdfeq0  18421  dpjf  18456  dpjlid  18460  dpjghm  18462  ablfac1eu  18472  islbs3  19155  lbsextlem4  19161  frlmsslss2  20114  frlmlbs  20136  mdetrlin  20408  mdetrsca  20409  mdetralt  20414  mdetmul  20429  smadiadetlem3lem0  20471  smadiadet  20476  clsval2  20854  hausllycmp  21297  qtoprest  21520  trfil3  21692  ufileu  21723  fclscf  21829  alexsublem  21848  blcld  22310  restmetu  22375  evth  22758  lebnumlem1  22760  lebnumlem2  22761  lebnumlem3  22762  cmmbl  23302  nulmbl2  23304  volinun  23314  volsup  23324  uniioombllem3  23353  uniioombllem5  23355  uniioombl  23357  itg1addlem5  23467  itg2cnlem2  23529  dvreslem  23673  dvres2lem  23674  dvaddbr  23701  dvmulbr  23702  dvrec  23718  dvexp3  23741  dveflem  23742  dvcnvrelem2  23781  uhgrspan1  26195  fprodeq02  29569  madjusmdetlem1  29893  indsum  30083  indsumin  30084  esumpad  30117  esumpad2  30118  measiun  30281  difelcarsg  30372  carsgclctunlem2  30381  tgoldbachgtde  30738  mthmpps  31479  dvreasin  33498  dvreacos  33499  areacirclem4  33503  ntrclsrcomplex  38333  clsk3nimkb  38338  ntrclsfveq1  38358  ntrclsiso  38365  ntrclsk2  38366  ntrclskb  38367  ntrclsk3  38368  ntrclsk13  38369  ntrneircomplex  38372  clsneircomplex  38401  clsneiel1  38406  neicvgrcomplex  38411  neicvgel1  38417  difmap  39399  difmapsn  39404  supminfxr2  39699  iccdifprioo  39742  limciccioolb  39853  lptioo2  39863  lptioo1  39864  limcicciooub  39869  dvdivcncf  40142  itgvol0  40184  itgcoscmulx  40185  itgsincmulx  40190  ismbl3  40203  stoweidlem28  40245  stoweidlem50  40267  dirkeritg  40319  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem39  40363  fourierdlem58  40381  fourierdlem68  40391  fourierdlem76  40399  fourierdlem102  40425  fourierdlem114  40437  pwsal  40535  salexct  40552  sge0fodjrnlem  40633  iundjiun  40677  meaunle  40681  meadjiunlem  40682  meaiunlelem  40685  meadif  40696  meaiuninclem  40697  meaiininclem  40700  carageniuncllem2  40736  caragencmpl  40749  hsphoidmvle2  40799  hsphoidmvle  40800  hoidmv1lelem2  40806  hspmbllem1  40840  hspmbllem3  40842  fdmdifeqresdif  42120  lincdifsn  42213  lincresunit2  42267  lincresunit3lem2  42269