Theorem ssdif 4140

Description: Difference law for subsets. (Contributed by NM, 28-May-1998.)

Assertion

Ref	Expression
ssdif	⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))

Proof of Theorem ssdif

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3976	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 612	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
3		eldif 3959	. . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶))
4		eldif 3959	. . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐶) → 𝑥 ∈ (𝐵 ∖ 𝐶)))
6	5	ssrdv 3989	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∈ wcel 2107   ∖ cdif 3946   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966

This theorem is referenced by:  ssdifd  4141  pssnn  9168  php  9210  phpOLD  9222  pssnnOLD  9265  fin1a2lem13  10407  axcclem  10452  isercolllem3  15613  mvdco  19313  dprdres  19898  dpjidcl  19928  ablfac1eulem  19942  cntzsdrg  20418  lspsnat  20758  lbsextlem2  20772  lbsextlem3  20773  cnsubdrglem  20996  mplmonmul  21591  clsconn  22934  2ndcdisj2  22961  kqdisj  23236  nulmbl2  25053  i1f1  25207  itg11  25208  itg1climres  25232  limcresi  25402  dvreslem  25426  dvres2lem  25427  dvaddbr  25455  dvmulbr  25456  lhop  25533  elqaa  25835  difres  31831  imadifxp  31832  xrge00  32187  elrspunidl  32546  eulerpartlemmf  33374  eulerpartlemgf  33378  gg-dvmulbr  35175  bj-2upln1upl  35905  pibt2  36298  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  cnambfre  36536  divrngidl  36896  dvrelog2  40929  dvrelog3  40930  dffltz  41376  cantnftermord  42070  omabs2  42082  radcnvrat  43073  fourierdlem62  44884