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

Theorem tpex 7686
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 4596 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2 prex 5394 . . 3 {𝐴, 𝐵} ∈ V
3 snex 5393 . . 3 {𝐶} ∈ V
42, 3unex 7685 . 2 ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
51, 4eqeltri 2834 1 {𝐴, 𝐵, 𝐶} ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3448  cun 3913  {csn 4591  {cpr 4593  {ctp 4595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-sn 4592  df-pr 4594  df-tp 4596  df-uni 4871
This theorem is referenced by:  fr3nr  7711  en3lp  9557  prdsval  17344  imasval  17400  fnfuc  17839  fucval  17853  setcval  17970  catcval  17993  estrcval  18018  estrreslem1  18031  estrreslem1OLD  18032  estrres  18034  fnxpc  18071  xpcval  18072  efmnd  18687  xrsex  20828  psrval  21333  om1val  24409  idlsrgval  32285  signswbase  33206  signswplusg  33207  ldualset  37616  erngset  39292  erngset-rN  39300  dvaset  39497  dvhset  39573  hlhilset  40426  rabren3dioph  41167  mendval  41539  clsk1indlem4  42390  clsk1indlem1  42391  rngcvalALTV  46333  ringcvalALTV  46379  lmod1zrnlvec  46649  mndtcval  47179
  Copyright terms: Public domain W3C validator