Theorem ssdif 4097

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2109   ∖ cdif 3902   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-dif 3908  df-ss 3922

This theorem is referenced by:  ssdifd  4098  pssnn  9092  php  9131  fin1a2lem13  10325  axcclem  10370  isercolllem3  15592  mvdco  19342  dprdres  19927  dpjidcl  19957  ablfac1eulem  19971  cntzsdrg  20705  lspsnat  21070  lbsextlem2  21084  lbsextlem3  21085  cnsubdrglem  21343  mplmonmul  21959  clsconn  23333  2ndcdisj2  23360  kqdisj  23635  nulmbl2  25453  i1f1  25607  itg11  25608  itg1climres  25631  limcresi  25802  dvreslem  25826  dvres2lem  25827  dvaddbr  25856  dvmulbr  25857  dvmulbrOLD  25858  lhop  25937  elqaa  26246  difres  32562  imadifxp  32563  xrge00  32981  elrspunidl  33378  eulerpartlemmf  34345  eulerpartlemgf  34349  bj-2upln1upl  37000  pibt2  37393  mblfinlem3  37641  mblfinlem4  37642  ismblfin  37643  cnambfre  37650  divrngidl  38010  dvrelog2  42040  dvrelog3  42041  readvrec2  42337  readvrec  42338  dffltz  42610  cantnftermord  43296  omabs2  43308  radcnvrat  44290  fourierdlem62  46153