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

Theorem ssdif 4139
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 3973 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 609 . . 3 (𝐴𝐵 → ((𝑥𝐴 ∧ ¬ 𝑥𝐶) → (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
3 eldif 3957 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐶))
4 eldif 3957 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐶))
52, 3, 43imtr4g 295 . 2 (𝐴𝐵 → (𝑥 ∈ (𝐴𝐶) → 𝑥 ∈ (𝐵𝐶)))
65ssrdv 3985 1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  wcel 2099  cdif 3944  wss 3947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-dif 3950  df-ss 3964
This theorem is referenced by:  ssdifd  4140  pssnn  9206  php  9244  phpOLD  9256  pssnnOLD  9299  fin1a2lem13  10455  axcclem  10500  isercolllem3  15671  mvdco  19443  dprdres  20028  dpjidcl  20058  ablfac1eulem  20072  cntzsdrg  20781  lspsnat  21126  lbsextlem2  21140  lbsextlem3  21141  cnsubdrglem  21415  mplmonmul  22043  clsconn  23425  2ndcdisj2  23452  kqdisj  23727  nulmbl2  25556  i1f1  25710  itg11  25711  itg1climres  25735  limcresi  25905  dvreslem  25929  dvres2lem  25930  dvaddbr  25959  dvmulbr  25960  dvmulbrOLD  25961  lhop  26040  elqaa  26350  difres  32520  imadifxp  32521  xrge00  32895  elrspunidl  33303  eulerpartlemmf  34209  eulerpartlemgf  34213  bj-2upln1upl  36731  pibt2  37124  mblfinlem3  37360  mblfinlem4  37361  ismblfin  37362  cnambfre  37369  divrngidl  37729  dvrelog2  41763  dvrelog3  41764  dffltz  42288  cantnftermord  42986  omabs2  42998  radcnvrat  43988  fourierdlem62  45789
  Copyright terms: Public domain W3C validator