Theorem ssdif 4106

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∈ wcel 2149   ∖ cdif 3910   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-ss 3930

This theorem is referenced by:  ssdifd  4107  pssnn  9149  php  9187  fin1a2lem13  10392  axcclem  10437  isercolllem3  15714  mvdco  19511  dprdres  20096  dpjidcl  20126  ablfac1eulem  20140  cntzsdrg  20879  lspsnat  21243  lbsextlem2  21257  lbsextlem3  21258  cnsubdrglem  21533  mplmonmul  22152  clsconn  23552  2ndcdisj2  23579  kqdisj  23854  nulmbl2  25660  i1f1  25814  itg11  25815  itg1climres  25838  limcresi  26009  dvreslem  26033  dvres2lem  26034  dvaddbr  26062  dvmulbr  26063  lhop  26140  elqaa  26448  difres  32882  imadifxp  32883  xrge00  33271  elrspunidl  33676  psrmonmul  33881  eulerpartlemmf  34706  eulerpartlemgf  34710  bj-2upln1upl  37544  pibt2  37946  mblfinlem3  38193  mblfinlem4  38194  ismblfin  38195  cnambfre  38202  divrngidl  38562  dvrelog2  42716  dvrelog3  42717  readvrec2  43005  readvrec  43006  dffltz  43251  cantnftermord  43932  omabs2  43944  radcnvrat  44909  fourierdlem62  46767