Theorem ssdif 4167

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2108   ∖ cdif 3973   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-ss 3993

This theorem is referenced by:  ssdifd  4168  pssnn  9234  php  9273  phpOLD  9285  fin1a2lem13  10481  axcclem  10526  isercolllem3  15715  mvdco  19487  dprdres  20072  dpjidcl  20102  ablfac1eulem  20116  cntzsdrg  20825  lspsnat  21170  lbsextlem2  21184  lbsextlem3  21185  cnsubdrglem  21459  mplmonmul  22077  clsconn  23459  2ndcdisj2  23486  kqdisj  23761  nulmbl2  25590  i1f1  25744  itg11  25745  itg1climres  25769  limcresi  25940  dvreslem  25964  dvres2lem  25965  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  lhop  26075  elqaa  26382  difres  32622  imadifxp  32623  xrge00  32998  elrspunidl  33421  eulerpartlemmf  34340  eulerpartlemgf  34344  bj-2upln1upl  36990  pibt2  37383  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  cnambfre  37628  divrngidl  37988  dvrelog2  42021  dvrelog3  42022  dffltz  42589  cantnftermord  43282  omabs2  43294  radcnvrat  44283  fourierdlem62  46089