Theorem ssdif 4099

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∈ wcel 2143   ∖ cdif 3903   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3909  df-ss 3923

This theorem is referenced by:  ssdifd  4100  pssnn  9154  php  9192  fin1a2lem13  10397  axcclem  10442  isercolllem3  15720  mvdco  19516  dprdres  20101  dpjidcl  20131  ablfac1eulem  20145  cntzsdrg  20886  lspsnat  21250  lbsextlem2  21264  lbsextlem3  21265  cnsubdrglem  21549  mplmonmul  22168  clsconn  23568  2ndcdisj2  23595  kqdisj  23870  nulmbl2  25676  i1f1  25830  itg11  25831  itg1climres  25854  limcresi  26025  dvreslem  26049  dvres2lem  26050  dvaddbr  26078  dvmulbr  26079  lhop  26156  elqaa  26464  difres  32926  imadifxp  32927  xrge00  33315  elrspunidl  33717  psrmonmul  33921  eulerpartlemmf  34746  eulerpartlemgf  34750  bj-2upln1upl  37641  pibt2  38044  mblfinlem3  38291  mblfinlem4  38292  ismblfin  38293  cnambfre  38300  divrngidl  38660  dvrelog2  42812  dvrelog3  42813  readvrec2  43103  readvrec  43104  dffltz  43349  cantnftermord  44030  omabs2  44042  radcnvrat  45007  fourierdlem62  46865