Theorem ssdif 4110

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2109   ∖ cdif 3914   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-ss 3934

This theorem is referenced by:  ssdifd  4111  pssnn  9138  php  9177  fin1a2lem13  10372  axcclem  10417  isercolllem3  15640  mvdco  19382  dprdres  19967  dpjidcl  19997  ablfac1eulem  20011  cntzsdrg  20718  lspsnat  21062  lbsextlem2  21076  lbsextlem3  21077  cnsubdrglem  21342  mplmonmul  21950  clsconn  23324  2ndcdisj2  23351  kqdisj  23626  nulmbl2  25444  i1f1  25598  itg11  25599  itg1climres  25622  limcresi  25793  dvreslem  25817  dvres2lem  25818  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  lhop  25928  elqaa  26237  difres  32536  imadifxp  32537  xrge00  32960  elrspunidl  33406  eulerpartlemmf  34373  eulerpartlemgf  34377  bj-2upln1upl  37019  pibt2  37412  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  cnambfre  37669  divrngidl  38029  dvrelog2  42059  dvrelog3  42060  readvrec2  42356  readvrec  42357  dffltz  42629  cantnftermord  43316  omabs2  43328  radcnvrat  44310  fourierdlem62  46173