Theorem ssdif 4085

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2114   ∖ cdif 3887   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-ss 3907

This theorem is referenced by:  ssdifd  4086  pssnn  9096  php  9134  fin1a2lem13  10325  axcclem  10370  isercolllem3  15620  mvdco  19411  dprdres  19996  dpjidcl  20026  ablfac1eulem  20040  cntzsdrg  20770  lspsnat  21135  lbsextlem2  21149  lbsextlem3  21150  cnsubdrglem  21408  mplmonmul  22024  clsconn  23405  2ndcdisj2  23432  kqdisj  23707  nulmbl2  25513  i1f1  25667  itg11  25668  itg1climres  25691  limcresi  25862  dvreslem  25886  dvres2lem  25887  dvaddbr  25915  dvmulbr  25916  lhop  25993  elqaa  26299  difres  32685  imadifxp  32686  xrge00  33089  elrspunidl  33503  psrmonmul  33709  eulerpartlemmf  34535  eulerpartlemgf  34539  bj-2upln1upl  37347  pibt2  37747  mblfinlem3  37994  mblfinlem4  37995  ismblfin  37996  cnambfre  38003  divrngidl  38363  dvrelog2  42517  dvrelog3  42518  readvrec2  42807  readvrec  42808  dffltz  43081  cantnftermord  43766  omabs2  43778  radcnvrat  44759  fourierdlem62  46614