Theorem ssdif 4153

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2105   ∖ cdif 3959   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-ss 3979

This theorem is referenced by:  ssdifd  4154  pssnn  9206  php  9244  phpOLD  9256  fin1a2lem13  10449  axcclem  10494  isercolllem3  15699  mvdco  19477  dprdres  20062  dpjidcl  20092  ablfac1eulem  20106  cntzsdrg  20819  lspsnat  21164  lbsextlem2  21178  lbsextlem3  21179  cnsubdrglem  21453  mplmonmul  22071  clsconn  23453  2ndcdisj2  23480  kqdisj  23755  nulmbl2  25584  i1f1  25738  itg11  25739  itg1climres  25763  limcresi  25934  dvreslem  25958  dvres2lem  25959  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  lhop  26069  elqaa  26378  difres  32619  imadifxp  32620  xrge00  32999  elrspunidl  33435  eulerpartlemmf  34356  eulerpartlemgf  34360  bj-2upln1upl  37006  pibt2  37399  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  cnambfre  37654  divrngidl  38014  dvrelog2  42045  dvrelog3  42046  readvrec2  42369  readvrec  42370  dffltz  42620  cantnftermord  43309  omabs2  43321  radcnvrat  44309  fourierdlem62  46123