Theorem ssdif 3888

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 3738	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 589	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
3		eldif 3725	. . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶))
4		eldif 3725	. . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 285	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐶) → 𝑥 ∈ (𝐵 ∖ 𝐶)))
6	5	ssrdv 3750	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∈ wcel 2139   ∖ cdif 3712   ⊆ wss 3715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-dif 3718  df-in 3722  df-ss 3729

This theorem is referenced by:  ssdifd  3889  php  8309  pssnn  8343  fin1a2lem13  9426  axcclem  9471  isercolllem3  14596  mvdco  18065  dprdres  18627  dpjidcl  18657  ablfac1eulem  18671  lspsnat  19347  lbsextlem2  19361  lbsextlem3  19362  mplmonmul  19666  cnsubdrglem  19999  clsconn  21435  2ndcdisj2  21462  kqdisj  21737  nulmbl2  23504  i1f1  23656  itg11  23657  itg1climres  23680  limcresi  23848  dvreslem  23872  dvres2lem  23873  dvaddbr  23900  dvmulbr  23901  lhop  23978  elqaa  24276  difres  29720  imadifxp  29721  xrge00  29995  eulerpartlemmf  30746  eulerpartlemgf  30750  bj-2upln1upl  33318  mblfinlem3  33761  mblfinlem4  33762  ismblfin  33763  cnambfre  33771  divrngidl  34140  cntzsdrg  38274  radcnvrat  39015  fourierdlem62  40888