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

Theorem ssdifssd 3732
Description: If 𝐴 is contained in 𝐵, then (𝐴𝐶) is also contained in 𝐵. Deduction form of ssdifss 3725. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
ssdifd.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
ssdifssd (𝜑 → (𝐴𝐶) ⊆ 𝐵)

Proof of Theorem ssdifssd
StepHypRef Expression
1 ssdifd.1 . 2 (𝜑𝐴𝐵)
2 ssdifss 3725 . 2 (𝐴𝐵 → (𝐴𝐶) ⊆ 𝐵)
31, 2syl 17 1 (𝜑 → (𝐴𝐶) ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  cdif 3557  wss 3560
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 3192  df-dif 3563  df-in 3567  df-ss 3574
This theorem is referenced by:  unblem1  8172  fin23lem26  9107  fin23lem29  9123  isf32lem8  9142  fprodfvdvdsd  15001  mrieqvlemd  16229  mrieqv2d  16239  mrissmrid  16241  mreexmrid  16243  mreexexlem2d  16245  mreexexlem4d  16247  acsfiindd  17117  ablfac1eulem  18411  lbspss  19022  lspsolv  19083  lsppratlem3  19089  lsppratlem4  19090  lspprat  19093  islbs2  19094  islbs3  19095  lbsextlem2  19099  lbsextlem3  19100  lbsextlem4  19101  lpss3  20888  islp3  20890  neitr  20924  restlp  20927  lpcls  21108  qtoprest  21460  ufinffr  21673  cldsubg  21854  xrge0gsumle  22576  bcthlem5  23065  rrxmval  23128  cmmbl  23242  nulmbl2  23244  shftmbl  23246  iundisj2  23257  uniiccdif  23286  uniiccmbl  23298  itg1val2  23391  itg1cl  23392  itg1ge0  23393  i1fadd  23402  itg1addlem5  23407  i1fmulc  23410  itg1mulc  23411  itg10a  23417  itg1ge0a  23418  itg1climres  23421  mbfi1fseqlem4  23425  itgss3  23521  limcdif  23580  limcnlp  23582  limcmpt2  23588  perfdvf  23607  dvcnp2  23623  dvaddbr  23641  dvmulbr  23642  dvferm1  23686  dvferm2  23688  ftc1lem6  23742  ig1peu  23869  ig1pdvds  23874  taylthlem1  24065  taylthlem2  24066  ulmdvlem3  24094  rlimcnp  24626  wilthlem2  24729  elpwdifcl  29246  iundisj2f  29289  ofpreima2  29350  iundisj2fi  29439  omsmeas  30208  eulerpartlemgs2  30265  ballotlemfrc  30411  cvmscld  31016  unbdqndv1  32194  lindsenlbs  33075  ftc1cnnc  33155  lsatfixedN  33815  dochsnkr  36280  hdmaprnlem4tN  36663  cntzsdrg  37292  limcrecl  39297  fperdvper  39470  ismbl3  39540  ovolsplit  39542  ismbl4  39547  stoweidlem57  39611  dirkercncflem3  39659  fourierdlem42  39703  fourierdlem46  39706  fourierdlem62  39722  caragenuncllem  40063  caragendifcl  40065  omelesplit  40069  carageniuncllem2  40073  carageniuncl  40074  caragenel2d  40083  hspmbllem3  40179  hspmbl  40180  ovnsplit  40199  vonvolmbllem  40211  vonvolmbl  40212  c0rnghm  41231  lincdifsn  41531  lindslinindsimp1  41564  lincresunit3lem2  41587
  Copyright terms: Public domain W3C validator