Theorem ssdif 4074

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904

This theorem is referenced by:  ssdifd  4075  pssnn  8951  php  8993  phpOLD  9005  pssnnOLD  9040  fin1a2lem13  10168  axcclem  10213  isercolllem3  15378  mvdco  19053  dprdres  19631  dpjidcl  19661  ablfac1eulem  19675  cntzsdrg  20070  lspsnat  20407  lbsextlem2  20421  lbsextlem3  20422  cnsubdrglem  20649  mplmonmul  21237  clsconn  22581  2ndcdisj2  22608  kqdisj  22883  nulmbl2  24700  i1f1  24854  itg11  24855  itg1climres  24879  limcresi  25049  dvreslem  25073  dvres2lem  25074  dvaddbr  25102  dvmulbr  25103  lhop  25180  elqaa  25482  difres  30939  imadifxp  30940  xrge00  31295  elrspunidl  31606  eulerpartlemmf  32342  eulerpartlemgf  32346  bj-2upln1upl  35214  pibt2  35588  mblfinlem3  35816  mblfinlem4  35817  ismblfin  35818  cnambfre  35825  divrngidl  36186  dvrelog2  40072  dvrelog3  40073  dffltz  40471  radcnvrat  41932  fourierdlem62  43709