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

Theorem ssdif 4037
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 3883 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 610 . . 3 (𝐴𝐵 → ((𝑥𝐴 ∧ ¬ 𝑥𝐶) → (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
3 eldif 3869 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐶))
4 eldif 3869 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐶))
52, 3, 43imtr4g 297 . 2 (𝐴𝐵 → (𝑥 ∈ (𝐴𝐶) → 𝑥 ∈ (𝐵𝐶)))
65ssrdv 3895 1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wcel 2081  cdif 3856  wss 3859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-dif 3862  df-in 3866  df-ss 3874
This theorem is referenced by:  ssdifd  4038  php  8548  pssnn  8582  fin1a2lem13  9680  axcclem  9725  isercolllem3  14857  mvdco  18304  dprdres  18867  dpjidcl  18897  ablfac1eulem  18911  cntzsdrg  19271  lspsnat  19607  lbsextlem2  19621  lbsextlem3  19622  mplmonmul  19932  cnsubdrglem  20278  clsconn  21722  2ndcdisj2  21749  kqdisj  22024  nulmbl2  23820  i1f1  23974  itg11  23975  itg1climres  23998  limcresi  24166  dvreslem  24190  dvres2lem  24191  dvaddbr  24218  dvmulbr  24219  lhop  24296  elqaa  24594  difres  30040  imadifxp  30041  xrge00  30347  eulerpartlemmf  31250  eulerpartlemgf  31254  bj-2upln1upl  33960  pibt2  34248  mblfinlem3  34481  mblfinlem4  34482  ismblfin  34483  cnambfre  34490  divrngidl  34857  dffltz  38787  radcnvrat  40203  fourierdlem62  42015
  Copyright terms: Public domain W3C validator