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

Theorem tpex 4556
Description: A triple of classes exists. (Contributed by NM, 10-Apr-1994.)
Assertion
Ref Expression
tpex  |-  { A ,  B ,  C }  e.  _V

Proof of Theorem tpex
StepHypRef Expression
1 df-tp 3682 . 2  |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
2 prex 4254 . . 3  |-  { A ,  B }  e.  _V
3 snex 4253 . . 3  |-  { C }  e.  _V
42, 3unex 4555 . 2  |-  ( { A ,  B }  u.  { C } )  e.  _V
51, 4eqeltri 2386 1  |-  { A ,  B ,  C }  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1701   _Vcvv 2822    u. cun 3184   {csn 3674   {cpr 3675   {ctp 3676
This theorem is referenced by:  fr3nr  4608  en3lp  7463  prdsval  13404  imasval  13463  fnfuc  13868  fucval  13881  setcval  13958  catcval  13977  fnxpc  13999  xpcval  14000  symgval  14820  psrval  16159  xrsex  16445  om1val  18581  rabren3dioph  26046  mendval  26639  wlkntrl  27466  constr2trl  27494  constr2pth  27497  2pthon  27498  2pthon3v  27500  constr3lem1  27529  constr3cyclpe  27547  3v3e3cycl2  27548  ldualset  29133  erngset  30807  erngset-rN  30815  dvaset  31012  dvhset  31089  hlhilset  31945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251  ax-un 4549
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-rex 2583  df-v 2824  df-dif 3189  df-un 3191  df-nul 3490  df-sn 3680  df-pr 3681  df-tp 3682  df-uni 3865
  Copyright terms: Public domain W3C validator