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

Theorem snsstp1 4320
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 4318 . . 3 {𝐴} ⊆ {𝐴, 𝐵}
2 ssun1 3759 . . 3 {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
31, 2sstri 3597 . 2 {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4 df-tp 4158 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
53, 4sseqtr4i 3622 1 {𝐴} ⊆ {𝐴, 𝐵, 𝐶}
Colors of variables: wff setvar class
Syntax hints:  cun 3558  wss 3560  {csn 4153  {cpr 4155  {ctp 4157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-v 3193  df-un 3565  df-in 3567  df-ss 3574  df-pr 4156  df-tp 4158
This theorem is referenced by:  fr3nr  6927  rngbase  15917  srngbase  15925  lmodbase  15934  ipsbase  15941  ipssca  15944  phlbase  15951  topgrpbas  15959  otpsbas  15968  otpsbasOLD  15972  odrngbas  15983  odrngtset  15986  prdssca  16032  prdsbas  16033  prdstset  16042  imasbas  16088  imassca  16095  imastset  16098  fucbas  16536  setcbas  16644  catcbas  16663  estrcbas  16681  xpcbas  16734  psrbas  19292  psrsca  19303  cnfldbas  19664  cnfldtset  19668  trkgbas  25239  signswch  30410  algbase  37215  clsk1indlem4  37810  clsk1indlem1  37811  rngcbasALTV  41244  ringcbasALTV  41307
  Copyright terms: Public domain W3C validator