Theorem ssdif 4040

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∈ wcel 2112   ∖ cdif 3850   ⊆ wss 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-dif 3856  df-in 3860  df-ss 3870

This theorem is referenced by:  ssdifd  4041  php  8808  pssnn  8824  pssnnOLD  8872  fin1a2lem13  9991  axcclem  10036  isercolllem3  15195  mvdco  18791  dprdres  19369  dpjidcl  19399  ablfac1eulem  19413  cntzsdrg  19800  lspsnat  20136  lbsextlem2  20150  lbsextlem3  20151  cnsubdrglem  20368  mplmonmul  20947  clsconn  22281  2ndcdisj2  22308  kqdisj  22583  nulmbl2  24387  i1f1  24541  itg11  24542  itg1climres  24566  limcresi  24736  dvreslem  24760  dvres2lem  24761  dvaddbr  24789  dvmulbr  24790  lhop  24867  elqaa  25169  difres  30612  imadifxp  30613  xrge00  30968  elrspunidl  31274  eulerpartlemmf  32008  eulerpartlemgf  32012  bj-2upln1upl  34900  pibt2  35274  mblfinlem3  35502  mblfinlem4  35503  ismblfin  35504  cnambfre  35511  divrngidl  35872  dvrelog2  39754  dvrelog3  39755  dffltz  40115  radcnvrat  41546  fourierdlem62  43327