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

Theorem tpex 4700
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 3814 . 2  |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
2 prex 4398 . . 3  |-  { A ,  B }  e.  _V
3 snex 4397 . . 3  |-  { C }  e.  _V
42, 3unex 4699 . 2  |-  ( { A ,  B }  u.  { C } )  e.  _V
51, 4eqeltri 2505 1  |-  { A ,  B ,  C }  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   _Vcvv 2948    u. cun 3310   {csn 3806   {cpr 3807   {ctp 3808
This theorem is referenced by:  fr3nr  4752  en3lp  7664  prdsval  13670  imasval  13729  fnfuc  14134  fucval  14147  setcval  14224  catcval  14243  fnxpc  14265  xpcval  14266  symgval  15086  psrval  16421  xrsex  16708  om1val  19047  wlkntrl  21554  constr2wlk  21590  constr2trl  21591  constr2spth  21592  constr2pth  21593  2pthon  21594  2pthon3v  21596  constr3lem1  21624  constr3cyclpe  21642  3v3e3cycl2  21643  rabren3dioph  26867  mendval  27459  usgra2adedgwlkon  28270  usg2wlk  28272  usg2wlkon  28273  ldualset  29860  erngset  31534  erngset-rN  31542  dvaset  31739  dvhset  31816  hlhilset  32672
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395  ax-un 4693
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-rex 2703  df-v 2950  df-dif 3315  df-un 3317  df-nul 3621  df-sn 3812  df-pr 3813  df-tp 3814  df-uni 4008
  Copyright terms: Public domain W3C validator