Theorem ssdif 4095

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 3928	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 620	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
3		eldif 3912	. . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶))
4		eldif 3912	. . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 298	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐶) → 𝑥 ∈ (𝐵 ∖ 𝐶)))
6	5	ssrdv 3940	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∈ wcel 2141   ∖ cdif 3899   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-dif 3905  df-ss 3919

This theorem is referenced by:  ssdifd  4096  pssnn  9131  php  9169  fin1a2lem13  10363  axcclem  10408  isercolllem3  15685  mvdco  19476  dprdres  20061  dpjidcl  20091  ablfac1eulem  20105  cntzsdrg  20839  lspsnat  21203  lbsextlem2  21217  lbsextlem3  21218  cnsubdrglem  21458  mplmonmul  22077  clsconn  23478  2ndcdisj2  23505  kqdisj  23780  nulmbl2  25586  i1f1  25740  itg11  25741  itg1climres  25764  limcresi  25935  dvreslem  25959  dvres2lem  25960  dvaddbr  25988  dvmulbr  25989  lhop  26066  elqaa  26374  difres  32760  imadifxp  32761  xrge00  33153  elrspunidl  33575  psrmonmul  33808  eulerpartlemmf  34633  eulerpartlemgf  34637  bj-2upln1upl  37470  pibt2  37872  mblfinlem3  38119  mblfinlem4  38120  ismblfin  38121  cnambfre  38128  divrngidl  38488  dvrelog2  42642  dvrelog3  42643  readvrec2  42931  readvrec  42932  dffltz  43177  cantnftermord  43858  omabs2  43870  radcnvrat  44851  fourierdlem62  46703