Theorem ssdif 4103

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 3937	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 611	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
3		eldif 3921	. . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶))
4		eldif 3921	. . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐶) → 𝑥 ∈ (𝐵 ∖ 𝐶)))
6	5	ssrdv 3949	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2109   ∖ cdif 3908   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914  df-ss 3928

This theorem is referenced by:  ssdifd  4104  pssnn  9109  php  9148  fin1a2lem13  10341  axcclem  10386  isercolllem3  15609  mvdco  19351  dprdres  19936  dpjidcl  19966  ablfac1eulem  19980  cntzsdrg  20687  lspsnat  21031  lbsextlem2  21045  lbsextlem3  21046  cnsubdrglem  21311  mplmonmul  21919  clsconn  23293  2ndcdisj2  23320  kqdisj  23595  nulmbl2  25413  i1f1  25567  itg11  25568  itg1climres  25591  limcresi  25762  dvreslem  25786  dvres2lem  25787  dvaddbr  25816  dvmulbr  25817  dvmulbrOLD  25818  lhop  25897  elqaa  26206  difres  32502  imadifxp  32503  xrge00  32926  elrspunidl  33372  eulerpartlemmf  34339  eulerpartlemgf  34343  bj-2upln1upl  36985  pibt2  37378  mblfinlem3  37626  mblfinlem4  37627  ismblfin  37628  cnambfre  37635  divrngidl  37995  dvrelog2  42025  dvrelog3  42026  readvrec2  42322  readvrec  42323  dffltz  42595  cantnftermord  43282  omabs2  43294  radcnvrat  44276  fourierdlem62  46139