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

Theorem tpex 7458
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 4564 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2 prex 5324 . . 3 {𝐴, 𝐵} ∈ V
3 snex 5323 . . 3 {𝐶} ∈ V
42, 3unex 7457 . 2 ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
51, 4eqeltri 2909 1 {𝐴, 𝐵, 𝐶} ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  Vcvv 3495  cun 3933  {csn 4559  {cpr 4561  {ctp 4563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-v 3497  df-dif 3938  df-un 3940  df-nul 4291  df-sn 4560  df-pr 4562  df-tp 4564  df-uni 4833
This theorem is referenced by:  fr3nr  7482  en3lp  9066  prdsval  16718  imasval  16774  fnfuc  17205  fucval  17218  setcval  17327  catcval  17346  estrcval  17364  estrreslem1  17377  estrres  17379  fnxpc  17416  xpcval  17417  symgval  18437  psrval  20072  xrsex  20490  om1val  23563  signswbase  31724  signswplusg  31725  ldualset  36143  erngset  37818  erngset-rN  37826  dvaset  38023  dvhset  38099  hlhilset  38952  rabren3dioph  39292  mendval  39663  clsk1indlem4  40274  clsk1indlem1  40275  efmnd  43939  rngcvalALTV  44130  ringcvalALTV  44176  lmod1zrnlvec  44447
  Copyright terms: Public domain W3C validator