Theorem tpex 6583

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 4032	. 2 |- { A , B , C } = ( { A , B } u. { C } )
2		prex 4689	. . 3 |- { A , B } e. _V
3		snex 4688	. . 3 |- { C } e. _V
4	2, 3	unex 6582	. 2 |- ( { A , B } u. { C } ) e. _V
5	1, 4	eqeltri 2551	1 |- { A , B , C } e. _V

Syntax hints:   e. wcel 1767   _Vcvv 3113   u. cun 3474   {csn 4027   {cpr 4029   {ctp 4031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686  ax-un 6576

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-rex 2820  df-v 3115  df-dif 3479  df-un 3481  df-nul 3786  df-sn 4028  df-pr 4030  df-tp 4032  df-uni 4246

This theorem is referenced by:  fr3nr  6599  en3lp  8033  prdsval  14710  imasval  14766  fnfuc  15172  fucval  15185  setcval  15262  catcval  15281  fnxpc  15303  xpcval  15304  symgval  16209  psrval  17810  xrsex  18232  om1val  21293  wlkntrl  24268  constr2wlk  24304  constr2trl  24305  constr2spth  24306  constr2pth  24307  2pthon  24308  2pthon3v  24310  usgra2adedgwlkon  24319  usg2wlk  24321  usg2wlkon  24322  constr3lem1  24349  constr3cyclpe  24367  3v3e3cycl2  24368  signswbase  28179  signswplusg  28180  rabren3dioph  30381  mendval  30765  lmod1zrnlvec  32194  ldualset  33940  erngset  35614  erngset-rN  35622  dvaset  35819  dvhset  35896  hlhilset  36752