Theorem ssdif 4070

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2108   ∖ cdif 3880   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900

This theorem is referenced by:  ssdifd  4071  php  8897  pssnn  8913  pssnnOLD  8969  fin1a2lem13  10099  axcclem  10144  isercolllem3  15306  mvdco  18968  dprdres  19546  dpjidcl  19576  ablfac1eulem  19590  cntzsdrg  19985  lspsnat  20322  lbsextlem2  20336  lbsextlem3  20337  cnsubdrglem  20561  mplmonmul  21147  clsconn  22489  2ndcdisj2  22516  kqdisj  22791  nulmbl2  24605  i1f1  24759  itg11  24760  itg1climres  24784  limcresi  24954  dvreslem  24978  dvres2lem  24979  dvaddbr  25007  dvmulbr  25008  lhop  25085  elqaa  25387  difres  30840  imadifxp  30841  xrge00  31197  elrspunidl  31508  eulerpartlemmf  32242  eulerpartlemgf  32246  bj-2upln1upl  35141  pibt2  35515  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  cnambfre  35752  divrngidl  36113  dvrelog2  40000  dvrelog3  40001  dffltz  40387  radcnvrat  41821  fourierdlem62  43599