Theorem ssdif 4037

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 3883	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 610	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
3		eldif 3869	. . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶))
4		eldif 3869	. . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 297	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐶) → 𝑥 ∈ (𝐵 ∖ 𝐶)))
6	5	ssrdv 3895	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∈ wcel 2081   ∖ cdif 3856   ⊆ wss 3859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-dif 3862  df-in 3866  df-ss 3874

This theorem is referenced by:  ssdifd  4038  php  8548  pssnn  8582  fin1a2lem13  9680  axcclem  9725  isercolllem3  14857  mvdco  18304  dprdres  18867  dpjidcl  18897  ablfac1eulem  18911  cntzsdrg  19271  lspsnat  19607  lbsextlem2  19621  lbsextlem3  19622  mplmonmul  19932  cnsubdrglem  20278  clsconn  21722  2ndcdisj2  21749  kqdisj  22024  nulmbl2  23820  i1f1  23974  itg11  23975  itg1climres  23998  limcresi  24166  dvreslem  24190  dvres2lem  24191  dvaddbr  24218  dvmulbr  24219  lhop  24296  elqaa  24594  difres  30040  imadifxp  30041  xrge00  30347  eulerpartlemmf  31250  eulerpartlemgf  31254  bj-2upln1upl  33960  pibt2  34248  mblfinlem3  34481  mblfinlem4  34482  ismblfin  34483  cnambfre  34490  divrngidl  34857  dffltz  38787  radcnvrat  40203  fourierdlem62  42015