Theorem ssdifd 4092

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

This proof depends on syntax axioms:   → wi 4   ∖ cdif 3896   ⊆ wss 3899

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-ss 3916

This theorem is used by:  ssdif2d  4095  domunsncan  9096  fin1a2lem13  10490  seqcoll2  14610  rpnnen2lem11  16392  coprmprod  16836  mrieqv2d  17813  mrissmrid  17815  mreexexlem4d  17821  acsfiindd  18727  chnind  18795  chnrev  18801  subdrgint  21060  lsppratlem3  21427  lsppratlem4  21428  f1lindf  22128  lpss3  23462  lpcls  23682  fin1aufil  24251  rrxmval  25726  rrxmetlem  25728  uniioombllem3  25906  i1fmul  26017  itg1addlem4  26020  itg1climres  26035  limciun  26214  ig1peu  26493  ig1pdvds  26498  fusgreghash2wspv  30936  indsumin  33428  pmtrcnel2  33651  pmtrcnelor  33652  tocyccntz  33705  elrspunidl  33978  elrspunsn  33979  sitgclg  34974  mthmpps  36347  poimirlem11  38549  poimirlem12  38550  poimirlem15  38553  dochfln0  42534  lcfl6  42557  lcfrlem16  42615  hdmaprnlem4N  42910  tfsconcatlem  44337  caragendifcl  47523