Theorem ssdifd 4117

Description: If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is contained in (𝐵 ∖ 𝐶). Deduction form of ssdif 4116. (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 4116	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))

Syntax hints:   → wi 4   ∖ cdif 3933   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939  df-in 3943  df-ss 3952

This theorem is referenced by:  ssdif2d  4120  domunsncan  8617  fin1a2lem13  9834  seqcoll2  13824  rpnnen2lem11  15577  coprmprod  16005  mrieqv2d  16910  mrissmrid  16912  mreexexlem4d  16918  acsfiindd  17787  subdrgint  19582  lsppratlem3  19921  lsppratlem4  19922  f1lindf  20966  lpss3  21752  lpcls  21972  fin1aufil  22540  rrxmval  24008  rrxmetlem  24010  uniioombllem3  24186  i1fmul  24297  itg1addlem4  24300  itg1climres  24315  limciun  24492  ig1peu  24765  ig1pdvds  24770  fusgreghash2wspv  28114  pmtrcnel2  30734  pmtrcnelor  30735  tocyccntz  30786  indsumin  31281  sitgclg  31600  mthmpps  32829  poimirlem11  34918  poimirlem12  34919  poimirlem15  34922  dochfln0  38628  lcfl6  38651  lcfrlem16  38709  hdmaprnlem4N  39004  caragendifcl  42816