Theorem difssd 4094

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

Assertion

Ref	Expression
difssd	⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐴)

Proof of Theorem difssd

Step	Hyp	Ref	Expression
1		difss 4093	. 2 ⊢ (𝐴 ∖ 𝐵) ⊆ 𝐴
2	1	a1i 11	1 ⊢ (𝜑 → (𝐴 ∖ 𝐵) ⊆ 𝐴)

This proof depends on syntax axioms:   → wi 4   ∖ cdif 3905   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-dif 3911  df-ss 3925

This theorem is used by:  uneqdifeq  4456  fpr1  8302  fofinf1o  9291  ackbij1lem12  10224  ssfin4  10304  enfin1ai  10378  fpwwe2  10638  wundif  10709  cshimadifsn  14877  indsum  15891  fprodn0f  16056  rpnnen2lem11  16290  mrieqvlemd  17695  mrieqv2d  17705  symgextfo  19502  symgextres  19505  symgfixelsi  19515  pmtrdifellem1  19556  pmtrdifellem2  19557  dprdfeq0  20104  dpjf  20139  dpjlid  20143  dpjghm  20145  ablfac1eu  20155  isdrng3lem1  20866  subdrgint  20921  islbs3  21294  lbsextlem4  21300  cnflddiv  21567  frlmsslss2  21940  frlmlbs  21962  selvvvval  22308  psdmul  22344  mdetrlin  22774  mdetrsca  22775  mdetralt  22780  mdetmul  22795  smadiadetlem3lem0  22837  smadiadet  22842  clsval2  23222  hausllycmp  23666  qtoprest  23889  trfil3  24060  ufileu  24091  fclscf  24197  alexsublem  24216  blcld  24677  restmetu  24742  evth  25133  lebnumlem1  25135  lebnumlem2  25136  lebnumlem3  25137  cmmbl  25708  nulmbl2  25710  volinun  25720  volsup  25730  uniioombllem3  25759  uniioombllem5  25761  uniioombl  25763  itg1addlem5  25874  itg2cnlem2  25936  dvreslem  26083  dvres2lem  26084  dvaddbr  26112  dvmulbr  26113  dvrec  26129  dvexp3  26152  dveflem  26153  dvcnvrelem2  26192  uhgrspan1  29668  unidifsnel  32896  fdifsupp  33045  fdifsuppconst  33049  fmptunsnop  33060  fprodeq02  33183  indsumin  33196  gsumhashmul  33400  suppgsumssiun  33405  symgcom2  33417  cycpmconjvlem  33474  domnprodn0  33611  dflringlem2  33798  rprmdvdsprod  33837  zringfrac  33857  ply1coedeg  33892  selvascl  33920  selvply1rhm0  33929  extvfvvcl  33938  extvfvcl  33939  evlextv  33945  psrmonprod  33955  esplyind  33978  esplyindfv  33979  esplyfvn  33980  vieta  33983  lindsunlem  34027  dimkerim  34030  madjusmdetlem1  34230  ist0cld  34236  esumpad  34458  esumpad2  34459  measiun  34621  difelcarsg  34713  carsgclctunlem2  34722  tgoldbachgtde  35060  f1resrcmplf1d  35488  satfv1lem  35866  dmopab3rexdif  35909  mthmpps  36086  dvreasin  38389  dvreacos  38390  areacirclem4  38394  sticksstones22  42967  evlselvlem  43352  evlselv  43353  ntrclsrcomplex  44793  ntrclsfveq1  44818  ntrclsiso  44825  ntrclsk2  44826  ntrclskb  44827  ntrclsk3  44828  ntrclsk13  44829  ntrneircomplex  44832  clsneircomplex  44861  clsneiel1  44866  neicvgrcomplex  44871  neicvgel1  44877  difmap  45955  difmapsn  45960  supminfxr2  46215  iccdifprioo  46264  limciccioolb  46369  lptioo2  46379  lptioo1  46380  limcicciooub  46383  dvdivcncf  46673  itgvol0  46714  itgcoscmulx  46715  itgsincmulx  46720  ismbl3  46732  stoweidlem28  46774  stoweidlem50  46796  dirkeritg  46848  dirkercncflem2  46850  dirkercncflem4  46852  fourierdlem39  46892  fourierdlem58  46910  fourierdlem68  46920  fourierdlem76  46928  fourierdlem102  46954  fourierdlem114  46966  pwsal  47061  salexct  47080  sge0fodjrnlem  47162  iundjiun  47206  meaunle  47210  meadjiunlem  47211  meaiunlelem  47214  meadif  47225  meaiuninclem  47226  meaiininclem  47232  carageniuncllem2  47268  caragencmpl  47281  hsphoidmvle2  47331  hsphoidmvle  47332  hoidmv1lelem2  47338  hspmbllem1  47372  hspmbllem3  47374  uhgrimisgrgric  48728  fdmdifeqresdif  49154  lincdifsn  49236  lincresunit2  49290  lincresunit3lem2  49292  iscnrm3rlem3  49752  iscnrm3rlem7  49756