Theorem ssdif 4081

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 3916	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 617	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶)))
3		eldif 3900	. . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐶))
4		eldif 3900	. . 3 ⊢ (𝑥 ∈ (𝐵 ∖ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 297	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∖ 𝐶) → 𝑥 ∈ (𝐵 ∖ 𝐶)))
6	5	ssrdv 3928	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∈ wcel 2119   ∖ cdif 3887   ⊆ wss 3890

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-dif 3893  df-ss 3907

This theorem is referenced by:  ssdifd  4082  pssnn  9100  php  9138  fin1a2lem13  10332  axcclem  10377  isercolllem3  15627  mvdco  19418  dprdres  20003  dpjidcl  20033  ablfac1eulem  20047  cntzsdrg  20781  lspsnat  21145  lbsextlem2  21159  lbsextlem3  21160  cnsubdrglem  21400  mplmonmul  22019  clsconn  23420  2ndcdisj2  23447  kqdisj  23722  nulmbl2  25528  i1f1  25682  itg11  25683  itg1climres  25706  limcresi  25877  dvreslem  25901  dvres2lem  25902  dvaddbr  25930  dvmulbr  25931  lhop  26008  elqaa  26313  difres  32696  imadifxp  32697  xrge00  33100  elrspunidl  33518  psrmonmul  33741  eulerpartlemmf  34566  eulerpartlemgf  34570  bj-2upln1upl  37384  pibt2  37786  mblfinlem3  38033  mblfinlem4  38034  ismblfin  38035  cnambfre  38042  divrngidl  38402  dvrelog2  42556  dvrelog3  42557  readvrec2  42845  readvrec  42846  dffltz  43091  cantnftermord  43772  omabs2  43784  radcnvrat  44765  fourierdlem62  46618