Theorem ssdif 4079

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∈ wcel 2110   ∖ cdif 3889   ⊆ wss 3892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-dif 3895  df-in 3899  df-ss 3909

This theorem is referenced by:  ssdifd  4080  pssnn  8931  php  8972  phpOLD  8985  pssnnOLD  9016  fin1a2lem13  10167  axcclem  10212  isercolllem3  15374  mvdco  19049  dprdres  19627  dpjidcl  19657  ablfac1eulem  19671  cntzsdrg  20066  lspsnat  20403  lbsextlem2  20417  lbsextlem3  20418  cnsubdrglem  20645  mplmonmul  21233  clsconn  22577  2ndcdisj2  22604  kqdisj  22879  nulmbl2  24696  i1f1  24850  itg11  24851  itg1climres  24875  limcresi  25045  dvreslem  25069  dvres2lem  25070  dvaddbr  25098  dvmulbr  25099  lhop  25176  elqaa  25478  difres  30933  imadifxp  30934  xrge00  31289  elrspunidl  31600  eulerpartlemmf  32336  eulerpartlemgf  32340  bj-2upln1upl  35208  pibt2  35582  mblfinlem3  35810  mblfinlem4  35811  ismblfin  35812  cnambfre  35819  divrngidl  36180  dvrelog2  40067  dvrelog3  40068  dffltz  40466  radcnvrat  41900  fourierdlem62  43678