Theorem ssdif 4104

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∈ wcel 2106   ∖ cdif 3910   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-dif 3916  df-in 3920  df-ss 3930

This theorem is referenced by:  ssdifd  4105  pssnn  9119  php  9161  phpOLD  9173  pssnnOLD  9216  fin1a2lem13  10357  axcclem  10402  isercolllem3  15563  mvdco  19241  dprdres  19821  dpjidcl  19851  ablfac1eulem  19865  cntzsdrg  20325  lspsnat  20665  lbsextlem2  20679  lbsextlem3  20680  cnsubdrglem  20885  mplmonmul  21474  clsconn  22818  2ndcdisj2  22845  kqdisj  23120  nulmbl2  24937  i1f1  25091  itg11  25092  itg1climres  25116  limcresi  25286  dvreslem  25310  dvres2lem  25311  dvaddbr  25339  dvmulbr  25340  lhop  25417  elqaa  25719  difres  31585  imadifxp  31586  xrge00  31947  elrspunidl  32279  eulerpartlemmf  33064  eulerpartlemgf  33068  bj-2upln1upl  35568  pibt2  35961  mblfinlem3  36190  mblfinlem4  36191  ismblfin  36192  cnambfre  36199  divrngidl  36560  dvrelog2  40594  dvrelog3  40595  dffltz  41030  cantnftermord  41713  omabs2  41725  radcnvrat  42716  fourierdlem62  44529