Theorem ssdif 4089

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2111   ∖ cdif 3894   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900  df-ss 3914

This theorem is referenced by:  ssdifd  4090  pssnn  9073  php  9111  fin1a2lem13  10298  axcclem  10343  isercolllem3  15569  mvdco  19352  dprdres  19937  dpjidcl  19967  ablfac1eulem  19981  cntzsdrg  20712  lspsnat  21077  lbsextlem2  21091  lbsextlem3  21092  cnsubdrglem  21350  mplmonmul  21966  clsconn  23340  2ndcdisj2  23367  kqdisj  23642  nulmbl2  25459  i1f1  25613  itg11  25614  itg1climres  25637  limcresi  25808  dvreslem  25832  dvres2lem  25833  dvaddbr  25862  dvmulbr  25863  dvmulbrOLD  25864  lhop  25943  elqaa  26252  difres  32572  imadifxp  32573  xrge00  32987  elrspunidl  33385  eulerpartlemmf  34380  eulerpartlemgf  34384  bj-2upln1upl  37058  pibt2  37451  mblfinlem3  37699  mblfinlem4  37700  ismblfin  37701  cnambfre  37708  divrngidl  38068  dvrelog2  42097  dvrelog3  42098  readvrec2  42394  readvrec  42395  dffltz  42667  cantnftermord  43353  omabs2  43365  radcnvrat  44347  fourierdlem62  46206