Theorem ssdif 4084

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2114   ∖ cdif 3886   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-ss 3906

This theorem is referenced by:  ssdifd  4085  pssnn  9103  php  9141  fin1a2lem13  10334  axcclem  10379  isercolllem3  15629  mvdco  19420  dprdres  20005  dpjidcl  20035  ablfac1eulem  20049  cntzsdrg  20779  lspsnat  21143  lbsextlem2  21157  lbsextlem3  21158  cnsubdrglem  21398  mplmonmul  22014  clsconn  23395  2ndcdisj2  23422  kqdisj  23697  nulmbl2  25503  i1f1  25657  itg11  25658  itg1climres  25681  limcresi  25852  dvreslem  25876  dvres2lem  25877  dvaddbr  25905  dvmulbr  25906  lhop  25983  elqaa  26288  difres  32670  imadifxp  32671  xrge00  33074  elrspunidl  33488  psrmonmul  33694  eulerpartlemmf  34519  eulerpartlemgf  34523  bj-2upln1upl  37331  pibt2  37733  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  cnambfre  37989  divrngidl  38349  dvrelog2  42503  dvrelog3  42504  readvrec2  42793  readvrec  42794  dffltz  43067  cantnftermord  43748  omabs2  43760  radcnvrat  44741  fourierdlem62  46596