Theorem ssdifd 4075

Description: If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is contained in (𝐵 ∖ 𝐶). Deduction form of ssdif 4074. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
ssdifd.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
ssdifd	⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))

Proof of Theorem ssdifd

Step	Hyp	Ref	Expression
1		ssdifd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		ssdif 4074	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))

Syntax hints:   → wi 4   ∖ cdif 3880   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-dif 3886  df-ss 3900

This theorem is referenced by:  ssdif2d  4078  domunsncan  9005  fin1a2lem13  10325  seqcoll2  14418  rpnnen2lem11  16182  coprmprod  16621  mrieqv2d  17596  mrissmrid  17598  mreexexlem4d  17604  acsfiindd  18510  chnind  18578  chnrev  18584  subdrgint  20775  lsppratlem3  21142  lsppratlem4  21143  f1lindf  21797  lpss3  23127  lpcls  23347  fin1aufil  23915  rrxmval  25390  rrxmetlem  25392  uniioombllem3  25570  i1fmul  25681  itg1addlem4  25684  itg1climres  25699  limciun  25879  ig1peu  26158  ig1pdvds  26163  fusgreghash2wspv  30423  indsumin  32940  pmtrcnel2  33171  pmtrcnelor  33172  tocyccntz  33225  elrspunidl  33511  elrspunsn  33512  sitgclg  34526  mthmpps  35810  poimirlem11  37998  poimirlem12  37999  poimirlem15  38002  dochfln0  41969  lcfl6  41992  lcfrlem16  42050  hdmaprnlem4N  42345  tfsconcatlem  43781  caragendifcl  46957