Theorem ssdif 4093

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2113   ∖ cdif 3895   ⊆ wss 3898

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-ss 3915

This theorem is referenced by:  ssdifd  4094  pssnn  9089  php  9127  fin1a2lem13  10314  axcclem  10359  isercolllem3  15581  mvdco  19365  dprdres  19950  dpjidcl  19980  ablfac1eulem  19994  cntzsdrg  20726  lspsnat  21091  lbsextlem2  21105  lbsextlem3  21106  cnsubdrglem  21364  mplmonmul  21982  clsconn  23365  2ndcdisj2  23392  kqdisj  23667  nulmbl2  25484  i1f1  25638  itg11  25639  itg1climres  25662  limcresi  25833  dvreslem  25857  dvres2lem  25858  dvaddbr  25887  dvmulbr  25888  dvmulbrOLD  25889  lhop  25968  elqaa  26277  difres  32601  imadifxp  32602  xrge00  33024  elrspunidl  33437  eulerpartlemmf  34460  eulerpartlemgf  34464  bj-2upln1upl  37141  pibt2  37534  mblfinlem3  37772  mblfinlem4  37773  ismblfin  37774  cnambfre  37781  divrngidl  38141  dvrelog2  42230  dvrelog3  42231  readvrec2  42531  readvrec  42532  dffltz  42792  cantnftermord  43477  omabs2  43489  radcnvrat  44471  fourierdlem62  46328