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

Theorem ssdif 4113
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 3958 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 610 . . 3 (𝐴𝐵 → ((𝑥𝐴 ∧ ¬ 𝑥𝐶) → (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
3 eldif 3943 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐶))
4 eldif 3943 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐶))
52, 3, 43imtr4g 297 . 2 (𝐴𝐵 → (𝑥 ∈ (𝐴𝐶) → 𝑥 ∈ (𝐵𝐶)))
65ssrdv 3970 1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wcel 2105  cdif 3930  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-dif 3936  df-in 3940  df-ss 3949
This theorem is referenced by:  ssdifd  4114  php  8689  pssnn  8724  fin1a2lem13  9822  axcclem  9867  isercolllem3  15011  mvdco  18502  dprdres  19079  dpjidcl  19109  ablfac1eulem  19123  cntzsdrg  19510  lspsnat  19846  lbsextlem2  19860  lbsextlem3  19861  mplmonmul  20173  cnsubdrglem  20524  clsconn  21966  2ndcdisj2  21993  kqdisj  22268  nulmbl2  24064  i1f1  24218  itg11  24219  itg1climres  24242  limcresi  24410  dvreslem  24434  dvres2lem  24435  dvaddbr  24462  dvmulbr  24463  lhop  24540  elqaa  24838  difres  30278  imadifxp  30279  xrge00  30600  eulerpartlemmf  31532  eulerpartlemgf  31536  bj-2upln1upl  34233  pibt2  34580  mblfinlem3  34812  mblfinlem4  34813  ismblfin  34814  cnambfre  34821  divrngidl  35187  dffltz  39149  radcnvrat  40523  fourierdlem62  42330
  Copyright terms: Public domain W3C validator