Theorem ssdif 4107

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

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

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 3449  df-dif 3917  df-ss 3931

This theorem is referenced by:  ssdifd  4108  pssnn  9132  php  9171  fin1a2lem13  10365  axcclem  10410  isercolllem3  15633  mvdco  19375  dprdres  19960  dpjidcl  19990  ablfac1eulem  20004  cntzsdrg  20711  lspsnat  21055  lbsextlem2  21069  lbsextlem3  21070  cnsubdrglem  21335  mplmonmul  21943  clsconn  23317  2ndcdisj2  23344  kqdisj  23619  nulmbl2  25437  i1f1  25591  itg11  25592  itg1climres  25615  limcresi  25786  dvreslem  25810  dvres2lem  25811  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  lhop  25921  elqaa  26230  difres  32529  imadifxp  32530  xrge00  32953  elrspunidl  33399  eulerpartlemmf  34366  eulerpartlemgf  34370  bj-2upln1upl  37012  pibt2  37405  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  cnambfre  37662  divrngidl  38022  dvrelog2  42052  dvrelog3  42053  readvrec2  42349  readvrec  42350  dffltz  42622  cantnftermord  43309  omabs2  43321  radcnvrat  44303  fourierdlem62  46166