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

Theorem snsstp1 4743
Description: A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)
Assertion
Ref Expression
snsstp1 {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Proof of Theorem snsstp1
StepHypRef Expression
1 snsspr1 4741 . . 3 {𝐴} ⊆ {𝐴, 𝐵}
2 ssun1 4147 . . 3 {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
31, 2sstri 3975 . 2 {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4 df-tp 4564 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
53, 4sseqtrri 4003 1 {𝐴} ⊆ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  cun 3933  wss 3935  {csn 4559  {cpr 4561  {ctp 4563
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 2793
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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-un 3940  df-in 3942  df-ss 3951  df-pr 4562  df-tp 4564
This theorem is referenced by:  fr3nr  7482  rngbase  16610  srngbase  16618  lmodbase  16627  ipsbase  16634  ipssca  16637  phlbase  16644  topgrpbas  16652  otpsbas  16659  odrngbas  16670  odrngtset  16673  prdssca  16719  prdsbas  16720  prdstset  16729  imasbas  16775  imassca  16782  imastset  16785  fucbas  17220  setcbas  17328  catcbas  17347  estrcbas  17365  psrbas  20088  psrsca  20099  cnfldbas  20479  cnfldtset  20483  trkgbas  26159  signswch  31731  algbase  39658  clsk1indlem4  40274  clsk1indlem1  40275  rngcbasALTV  44152  ringcbasALTV  44215
  Copyright terms: Public domain W3C validator