Theorem ssdif 4098

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2146   ∖ cdif 3903   ⊆ wss 3906

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-ss 3923

This theorem is used by:  ssdifd  4099  pssnn  9156  php  9194  fin1a2lem13  10407  axcclem  10452  isercolllem3  15737  mvdco  19538  dprdres  20123  dpjidcl  20153  ablfac1eulem  20167  cntzsdrg  20934  lspsnat  21298  lbsextlem2  21312  lbsextlem3  21313  cnsubdrglem  21597  mplmonmul  22216  clsconn  23616  2ndcdisj2  23643  kqdisj  23918  nulmbl2  25724  i1f1  25878  itg11  25879  itg1climres  25902  limcresi  26073  dvreslem  26097  dvres2lem  26098  dvaddbr  26126  dvmulbr  26127  lhop  26204  elqaa  26512  difres  32974  imadifxp  32975  xrge00  33357  elrspunidl  33759  psrmonmul  33963  eulerpartlemmf  34789  eulerpartlemgf  34793  bj-2upln1upl  37693  pibt2  38096  mblfinlem3  38343  mblfinlem4  38344  ismblfin  38345  cnambfre  38352  divrngidl  38712  dvrelog2  42864  dvrelog3  42865  readvrec2  43155  readvrec  43156  dffltz  43399  cantnftermord  44080  omabs2  44092  radcnvrat  45057  fourierdlem62  46915