Theorem ssdifd 4136

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

Syntax hints:   → wi 4   ∖ cdif 3942   ⊆ wss 3945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-dif 3948  df-in 3952  df-ss 3962

This theorem is referenced by:  ssdif2d  4139  domunsncan  9090  fin1a2lem13  10429  seqcoll2  14452  rpnnen2lem11  16194  coprmprod  16625  mrieqv2d  17612  mrissmrid  17614  mreexexlem4d  17620  acsfiindd  18538  subdrgint  20684  lsppratlem3  21030  lsppratlem4  21031  f1lindf  21749  lpss3  23041  lpcls  23261  fin1aufil  23829  rrxmval  25326  rrxmetlem  25328  uniioombllem3  25507  i1fmul  25618  itg1addlem4  25621  itg1addlem4OLD  25622  itg1climres  25637  limciun  25816  ig1peu  26102  ig1pdvds  26107  fusgreghash2wspv  30138  pmtrcnel2  32807  pmtrcnelor  32808  tocyccntz  32859  elrspunidl  33138  elrspunsn  33139  indsumin  33635  sitgclg  33956  mthmpps  35186  poimirlem11  37098  poimirlem12  37099  poimirlem15  37102  dochfln0  40944  lcfl6  40967  lcfrlem16  41025  hdmaprnlem4N  41320  tfsconcatlem  42759  caragendifcl  45896

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »