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

Theorem snsstp1 4733
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 4731 . . 3 {𝐴} ⊆ {𝐴, 𝐵}
2 ssun1 4133 . . 3 {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
31, 2sstri 3961 . 2 {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4 df-tp 4554 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
53, 4sseqtrri 3989 1 {𝐴} ⊆ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  cun 3917  wss 3919  {csn 4549  {cpr 4551  {ctp 4553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924  df-in 3926  df-ss 3936  df-pr 4552  df-tp 4554
This theorem is referenced by:  fr3nr  7484  rngbase  16616  srngbase  16624  lmodbase  16633  ipsbase  16640  ipssca  16643  phlbase  16650  topgrpbas  16658  otpsbas  16665  odrngbas  16676  odrngtset  16679  prdssca  16725  prdsbas  16726  prdstset  16735  imasbas  16781  imassca  16788  imastset  16791  fucbas  17226  setcbas  17334  catcbas  17353  estrcbas  17371  psrbas  20151  psrsca  20162  cnfldbas  20542  cnfldtset  20546  trkgbas  26235  signswch  31856  algbase  39975  clsk1indlem4  40603  clsk1indlem1  40604  rngcbasALTV  44470  ringcbasALTV  44533
  Copyright terms: Public domain W3C validator