Theorem tpex 6602

Description: An unordered triple of classes exists. (Contributed by NM, 10-Apr-1994.)

Assertion

Ref	Expression
tpex	|- { A , B , C } e. _V

Proof of Theorem tpex

Step	Hyp	Ref	Expression
1		df-tp 4002	. 2 |- { A , B , C } = ( { A , B } u. { C } )
2		prex 4661	. . 3 |- { A , B } e. _V
3		snex 4660	. . 3 |- { C } e. _V
4	2, 3	unex 6601	. 2 |- ( { A , B } u. { C } ) e. _V
5	1, 4	eqeltri 2507	1 |- { A , B , C } e. _V

Syntax hints:   e. wcel 1869   _Vcvv 3082   u. cun 3435   {csn 3997   {cpr 3999   {ctp 4001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pr 4658  ax-un 6595

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-rex 2782  df-v 3084  df-dif 3440  df-un 3442  df-nul 3763  df-sn 3998  df-pr 4000  df-tp 4002  df-uni 4218

This theorem is referenced by:  fr3nr  6618  en3lp  8125  prdsval  15346  imasval  15404  imasvalOLD  15405  fnfuc  15843  fucval  15856  setcval  15965  catcval  15984  estrcval  16002  estrreslem1  16015  estrres  16017  fnxpc  16054  xpcval  16055  symgval  17013  psrval  18579  xrsex  18976  om1val  22053  wlkntrl  25284  constr2trl  25321  constr2spth  25322  constr2pth  25323  2pthon  25324  2pthon3v  25326  usgra2adedgwlkon  25335  usg2wlk  25337  usg2wlkon  25338  constr3lem1  25365  constr3cyclpe  25383  3v3e3cycl2  25384  signswbase  29445  signswplusg  29446  ldualset  32654  erngset  34330  erngset-rN  34338  dvaset  34535  dvhset  34612  hlhilset  35468  rabren3dioph  35621  mendval  36013  rngcvalALTV  39305  ringcvalALTV  39351  lmod1zrnlvec  39631