Theorem ssdif 4080

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 3902	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 623	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
3		eldif 4049	. . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶))
4		eldif 4049	. . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐶) → 𝑥 ∈ (𝐵 ∖ 𝐶)))
6	5	ssrdv 3914	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2144   ⊆ wss 3895   ∖ cdif 4045

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-dif 4047

This theorem is used by:  ssdifd  4081  pssnn  9184  php  9222  fin1a2lem13  10490  axcclem  10535  isercolllem3  15834  mvdco  19659  dprdres  20244  dpjidcl  20274  ablfac1eulem  20288  cntzsdrg  21059  lspsnat  21423  lbsextlem2  21437  lbsextlem3  21438  cnsubdrglem  21724  mplmonmul  22345  clsconn  23748  2ndcdisj2  23776  kqdisj  24051  nulmbl2  25857  i1f1  26011  itg11  26012  itg1climres  26035  limcresi  26205  dvreslem  26229  dvres2lem  26230  dvaddbr  26258  dvmulbr  26259  lhop  26336  elqaa  26645  difres  33194  imadifxp  33195  xrge00  33575  elrspunidl  33978  psrmonmul  34182  eulerpartlemmf  35007  eulerpartlemgf  35011  bj-2upln1upl  37937  pibt2  38341  mblfinlem3  38578  mblfinlem4  38579  ismblfin  38580  cnambfre  38587  divrngidl  38963  dvrelog2  43115  dvrelog3  43116  readvrec2  43413  readvrec  43414  dffltz  43671  cantnftermord  44322  omabs2  44334  radcnvrat  45298  fourierdlem62  47178