Theorem ssdif 4091

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2145   ∖ cdif 3896   ⊆ wss 3899

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-ss 3916

This theorem is used by:  ssdifd  4092  pssnn  9177  php  9215  fin1a2lem13  10483  axcclem  10528  isercolllem3  15827  mvdco  19652  dprdres  20237  dpjidcl  20267  ablfac1eulem  20281  cntzsdrg  21052  lspsnat  21416  lbsextlem2  21430  lbsextlem3  21431  cnsubdrglem  21717  mplmonmul  22338  clsconn  23741  2ndcdisj2  23769  kqdisj  24044  nulmbl2  25850  i1f1  26004  itg11  26005  itg1climres  26028  limcresi  26198  dvreslem  26222  dvres2lem  26223  dvaddbr  26251  dvmulbr  26252  lhop  26329  elqaa  26638  difres  33187  imadifxp  33188  xrge00  33568  elrspunidl  33971  psrmonmul  34175  eulerpartlemmf  35000  eulerpartlemgf  35004  bj-2upln1upl  37917  pibt2  38320  mblfinlem3  38557  mblfinlem4  38558  ismblfin  38559  cnambfre  38566  divrngidl  38942  dvrelog2  43094  dvrelog3  43095  readvrec2  43392  readvrec  43393  dffltz  43650  cantnftermord  44306  omabs2  44318  radcnvrat  45283  fourierdlem62  47147