Theorem ssdif 4083

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2147   ⊆ wss 3900   ∖ cdif 4048

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-dif 4050

This theorem is used by:  ssdifd  4084  pssnn  9222  php  9260  fin1a2lem13  10529  axcclem  10574  isercolllem3  15878  mvdco  19710  dprdres  20295  dpjidcl  20325  ablfac1eulem  20339  cntzsdrg  21110  lspsnat  21474  lbsextlem2  21488  lbsextlem3  21489  cnsubdrglem  21776  mplmonmul  22400  clsconn  23803  2ndcdisj2  23831  kqdisj  24106  nulmbl2  25912  i1f1  26066  itg11  26067  itg1climres  26090  limcresi  26260  dvreslem  26284  dvres2lem  26285  dvaddbr  26313  dvmulbr  26314  lhop  26391  elqaa  26702  difres  33292  imadifxp  33293  xrge00  33674  elrspunidl  34082  psrmonmul  34293  eulerpartlemmf  35118  eulerpartlemgf  35122  bj-2upln1upl  38152  pibt2  38608  mblfinlem3  38845  mblfinlem4  38846  ismblfin  38847  cnambfre  38854  divrngidl  39228  dvrelog2  43380  dvrelog3  43381  readvrec2  43678  readvrec  43679  dffltz  43936  cantnftermord  44583  omabs2  44595  radcnvrat  45559  fourierdlem62  47451