Theorem ssdif 4139

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   ∈ wcel 2099   ∖ cdif 3944   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-dif 3950  df-ss 3964

This theorem is referenced by:  ssdifd  4140  pssnn  9206  php  9244  phpOLD  9256  pssnnOLD  9299  fin1a2lem13  10455  axcclem  10500  isercolllem3  15671  mvdco  19443  dprdres  20028  dpjidcl  20058  ablfac1eulem  20072  cntzsdrg  20781  lspsnat  21126  lbsextlem2  21140  lbsextlem3  21141  cnsubdrglem  21415  mplmonmul  22043  clsconn  23425  2ndcdisj2  23452  kqdisj  23727  nulmbl2  25556  i1f1  25710  itg11  25711  itg1climres  25735  limcresi  25905  dvreslem  25929  dvres2lem  25930  dvaddbr  25959  dvmulbr  25960  dvmulbrOLD  25961  lhop  26040  elqaa  26350  difres  32520  imadifxp  32521  xrge00  32895  elrspunidl  33303  eulerpartlemmf  34209  eulerpartlemgf  34213  bj-2upln1upl  36731  pibt2  37124  mblfinlem3  37360  mblfinlem4  37361  ismblfin  37362  cnambfre  37369  divrngidl  37729  dvrelog2  41763  dvrelog3  41764  dffltz  42288  cantnftermord  42986  omabs2  42998  radcnvrat  43988  fourierdlem62  45789