Theorem ssdif 4115

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∈ wcel 2110   ∖ cdif 3932   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3938  df-in 3942  df-ss 3951

This theorem is referenced by:  ssdifd  4116  php  8695  pssnn  8730  fin1a2lem13  9828  axcclem  9873  isercolllem3  15017  mvdco  18567  dprdres  19144  dpjidcl  19174  ablfac1eulem  19188  cntzsdrg  19575  lspsnat  19911  lbsextlem2  19925  lbsextlem3  19926  mplmonmul  20239  cnsubdrglem  20590  clsconn  22032  2ndcdisj2  22059  kqdisj  22334  nulmbl2  24131  i1f1  24285  itg11  24286  itg1climres  24309  limcresi  24477  dvreslem  24501  dvres2lem  24502  dvaddbr  24529  dvmulbr  24530  lhop  24607  elqaa  24905  difres  30344  imadifxp  30345  xrge00  30668  eulerpartlemmf  31628  eulerpartlemgf  31632  bj-2upln1upl  34331  pibt2  34692  mblfinlem3  34925  mblfinlem4  34926  ismblfin  34927  cnambfre  34934  divrngidl  35300  dffltz  39264  radcnvrat  40639  fourierdlem62  42447