Theorem ssdif 4096

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2113   ∖ cdif 3898   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-ss 3918

This theorem is referenced by:  ssdifd  4097  pssnn  9093  php  9131  fin1a2lem13  10322  axcclem  10367  isercolllem3  15590  mvdco  19374  dprdres  19959  dpjidcl  19989  ablfac1eulem  20003  cntzsdrg  20735  lspsnat  21100  lbsextlem2  21114  lbsextlem3  21115  cnsubdrglem  21373  mplmonmul  21991  clsconn  23374  2ndcdisj2  23401  kqdisj  23676  nulmbl2  25493  i1f1  25647  itg11  25648  itg1climres  25671  limcresi  25842  dvreslem  25866  dvres2lem  25867  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  lhop  25977  elqaa  26286  difres  32675  imadifxp  32676  xrge00  33096  elrspunidl  33509  eulerpartlemmf  34532  eulerpartlemgf  34536  bj-2upln1upl  37225  pibt2  37622  mblfinlem3  37860  mblfinlem4  37861  ismblfin  37862  cnambfre  37869  divrngidl  38229  dvrelog2  42318  dvrelog3  42319  readvrec2  42616  readvrec  42617  dffltz  42877  cantnftermord  43562  omabs2  43574  radcnvrat  44555  fourierdlem62  46412