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

Theorem tpex 7102
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 4318 . 2 {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2 prex 5036 . . 3 {𝐴, 𝐵} ∈ V
3 snex 5035 . . 3 {𝐶} ∈ V
42, 3unex 7101 . 2 ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
51, 4eqeltri 2844 1 {𝐴, 𝐵, 𝐶} ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2143  Vcvv 3348  cun 3718  {csn 4313  {cpr 4315  {ctp 4317
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1868  ax-4 1883  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2145  ax-9 2152  ax-10 2172  ax-11 2188  ax-12 2201  ax-13 2406  ax-ext 2749  ax-sep 4911  ax-nul 4919  ax-pr 5033  ax-un 7094
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1632  df-ex 1851  df-nf 1856  df-sb 2048  df-clab 2756  df-cleq 2762  df-clel 2765  df-nfc 2900  df-rex 3065  df-v 3350  df-dif 3723  df-un 3725  df-nul 4061  df-sn 4314  df-pr 4316  df-tp 4318  df-uni 4572
This theorem is referenced by:  fr3nr  7124  en3lp  8671  prdsval  16329  imasval  16385  fnfuc  16818  fucval  16831  setcval  16940  catcval  16959  estrcval  16977  estrreslem1  16990  estrresOLD  16992  estrres  16993  fnxpc  17030  xpcval  17031  symgval  18012  psrval  19583  xrsex  19982  om1val  23055  signswbase  30972  signswplusg  30973  ldualset  34934  erngset  36609  erngset-rN  36617  dvaset  36814  dvhset  36891  hlhilset  37744  rabren3dioph  37905  mendval  38279  clsk1indlem4  38868  clsk1indlem1  38869  rngcvalALTV  42486  ringcvalALTV  42532  lmod1zrnlvec  42808
  Copyright terms: Public domain W3C validator