MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssdif Structured version   Visualization version   GIF version

Theorem ssdif 4070
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.
StepHypRef Expression
1 ssel 3911 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 613 . . 3 (𝐴𝐵 → ((𝑥𝐴 ∧ ¬ 𝑥𝐶) → (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
3 eldif 3894 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐶))
4 eldif 3894 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐶))
52, 3, 43imtr4g 299 . 2 (𝐴𝐵 → (𝑥 ∈ (𝐴𝐶) → 𝑥 ∈ (𝐵𝐶)))
65ssrdv 3924 1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  wcel 2112  cdif 3881  wss 3884
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-dif 3887  df-in 3891  df-ss 3901
This theorem is referenced by:  ssdifd  4071  php  8689  pssnn  8724  fin1a2lem13  9827  axcclem  9872  isercolllem3  15019  mvdco  18569  dprdres  19147  dpjidcl  19177  ablfac1eulem  19191  cntzsdrg  19578  lspsnat  19914  lbsextlem2  19928  lbsextlem3  19929  cnsubdrglem  20146  mplmonmul  20708  clsconn  22039  2ndcdisj2  22066  kqdisj  22341  nulmbl2  24144  i1f1  24298  itg11  24299  itg1climres  24322  limcresi  24492  dvreslem  24516  dvres2lem  24517  dvaddbr  24545  dvmulbr  24546  lhop  24623  elqaa  24922  difres  30367  imadifxp  30368  xrge00  30724  elrspunidl  31018  eulerpartlemmf  31747  eulerpartlemgf  31751  bj-2upln1upl  34461  pibt2  34835  mblfinlem3  35095  mblfinlem4  35096  ismblfin  35097  cnambfre  35104  divrngidl  35465  dffltz  39608  radcnvrat  41011  fourierdlem62  42803
  Copyright terms: Public domain W3C validator