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

Theorem tpex 6911
Description: An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.)
Assertion
Ref Expression
tpex {𝐴, 𝐵, 𝐶} ∈ V

Proof of Theorem tpex
StepHypRef Expression
1 df-tp 4158 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2 prex 4875 . . 3 {𝐴, 𝐵} ∈ V
3 snex 4874 . . 3 {𝐶} ∈ V
42, 3unex 6910 . 2 ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
51, 4eqeltri 2700 1 {𝐴, 𝐵, 𝐶} ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1992  Vcvv 3191  cun 3558  {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-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pr 4872  ax-un 6903
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-rex 2918  df-v 3193  df-dif 3563  df-un 3565  df-nul 3897  df-sn 4154  df-pr 4156  df-tp 4158  df-uni 4408
This theorem is referenced by:  fr3nr  6927  en3lp  8458  prdsval  16031  imasval  16087  fnfuc  16521  fucval  16534  setcval  16643  catcval  16662  estrcval  16680  estrreslem1  16693  estrres  16695  fnxpc  16732  xpcval  16733  symgval  17715  psrval  19276  xrsex  19675  om1val  22733  signswbase  30403  signswplusg  30404  ldualset  33878  erngset  35554  erngset-rN  35562  dvaset  35759  dvhset  35836  hlhilset  36692  rabren3dioph  36845  mendval  37220  clsk1indlem4  37810  clsk1indlem1  37811  rngcvalALTV  41222  ringcvalALTV  41268  lmod1zrnlvec  41545
  Copyright terms: Public domain W3C validator