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

Theorem tpex 7463
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 4569 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2 prex 5329 . . 3 {𝐴, 𝐵} ∈ V
3 snex 5328 . . 3 {𝐶} ∈ V
42, 3unex 7462 . 2 ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
51, 4eqeltri 2914 1 {𝐴, 𝐵, 𝐶} ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3500  cun 3938  {csn 4564  {cpr 4566  {ctp 4568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326  ax-un 7455
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rex 3149  df-v 3502  df-dif 3943  df-un 3945  df-nul 4296  df-sn 4565  df-pr 4567  df-tp 4569  df-uni 4838
This theorem is referenced by:  fr3nr  7487  en3lp  9071  prdsval  16723  imasval  16779  fnfuc  17210  fucval  17223  setcval  17332  catcval  17351  estrcval  17369  estrreslem1  17382  estrres  17384  fnxpc  17421  xpcval  17422  symgval  18442  psrval  20077  xrsex  20495  om1val  23568  signswbase  31729  signswplusg  31730  ldualset  36147  erngset  37822  erngset-rN  37830  dvaset  38027  dvhset  38103  hlhilset  38956  rabren3dioph  39296  mendval  39667  clsk1indlem4  40278  clsk1indlem1  40279  efmnd  43943  rngcvalALTV  44134  ringcvalALTV  44180  lmod1zrnlvec  44451
  Copyright terms: Public domain W3C validator