Theorem ssdif 4091

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2145   ∖ cdif 3896   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-ss 3916

This theorem is used by:  ssdifd  4092  pssnn  9163  php  9201  fin1a2lem13  10414  axcclem  10459  isercolllem3  15754  mvdco  19572  dprdres  20157  dpjidcl  20187  ablfac1eulem  20201  cntzsdrg  20968  lspsnat  21332  lbsextlem2  21346  lbsextlem3  21347  cnsubdrglem  21631  mplmonmul  22252  clsconn  23655  2ndcdisj2  23683  kqdisj  23958  nulmbl2  25764  i1f1  25918  itg11  25919  itg1climres  25942  limcresi  26112  dvreslem  26136  dvres2lem  26137  dvaddbr  26165  dvmulbr  26166  lhop  26243  elqaa  26554  difres  33073  imadifxp  33074  xrge00  33454  elrspunidl  33856  psrmonmul  34060  eulerpartlemmf  34886  eulerpartlemgf  34890  bj-2upln1upl  37768  pibt2  38171  mblfinlem3  38408  mblfinlem4  38409  ismblfin  38410  cnambfre  38417  divrngidl  38778  dvrelog2  42930  dvrelog3  42931  readvrec2  43236  readvrec  43237  dffltz  43480  cantnftermord  44161  omabs2  44173  radcnvrat  45138  fourierdlem62  46996