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

Theorem ssdif 3888
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 3738 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
21anim1d 589 . . 3 (𝐴𝐵 → ((𝑥𝐴 ∧ ¬ 𝑥𝐶) → (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
3 eldif 3725 . . 3 (𝑥 ∈ (𝐴𝐶) ↔ (𝑥𝐴 ∧ ¬ 𝑥𝐶))
4 eldif 3725 . . 3 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐶))
52, 3, 43imtr4g 285 . 2 (𝐴𝐵 → (𝑥 ∈ (𝐴𝐶) → 𝑥 ∈ (𝐵𝐶)))
65ssrdv 3750 1 (𝐴𝐵 → (𝐴𝐶) ⊆ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  wcel 2139  cdif 3712  wss 3715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-dif 3718  df-in 3722  df-ss 3729
This theorem is referenced by:  ssdifd  3889  php  8309  pssnn  8343  fin1a2lem13  9426  axcclem  9471  isercolllem3  14596  mvdco  18065  dprdres  18627  dpjidcl  18657  ablfac1eulem  18671  lspsnat  19347  lbsextlem2  19361  lbsextlem3  19362  mplmonmul  19666  cnsubdrglem  19999  clsconn  21435  2ndcdisj2  21462  kqdisj  21737  nulmbl2  23504  i1f1  23656  itg11  23657  itg1climres  23680  limcresi  23848  dvreslem  23872  dvres2lem  23873  dvaddbr  23900  dvmulbr  23901  lhop  23978  elqaa  24276  difres  29720  imadifxp  29721  xrge00  29995  eulerpartlemmf  30746  eulerpartlemgf  30750  bj-2upln1upl  33318  mblfinlem3  33761  mblfinlem4  33762  ismblfin  33763  cnambfre  33771  divrngidl  34140  cntzsdrg  38274  radcnvrat  39015  fourierdlem62  40888
  Copyright terms: Public domain W3C validator