Theorem tpex 6590

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 3973	. 2 |- { A , B , C } = ( { A , B } u. { C } )
2		prex 4642	. . 3 |- { A , B } e. _V
3		snex 4641	. . 3 |- { C } e. _V
4	2, 3	unex 6589	. 2 |- ( { A , B } u. { C } ) e. _V
5	1, 4	eqeltri 2525	1 |- { A , B , C } e. _V

Syntax hints:   e. wcel 1887   _Vcvv 3045   u. cun 3402   {csn 3968   {cpr 3970   {ctp 3972

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pr 4639  ax-un 6583

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-rex 2743  df-v 3047  df-dif 3407  df-un 3409  df-nul 3732  df-sn 3969  df-pr 3971  df-tp 3973  df-uni 4199

This theorem is referenced by:  fr3nr  6606  en3lp  8121  prdsval  15353  imasval  15411  imasvalOLD  15412  fnfuc  15850  fucval  15863  setcval  15972  catcval  15991  estrcval  16009  estrreslem1  16022  estrres  16024  fnxpc  16061  xpcval  16062  symgval  17020  psrval  18586  xrsex  18983  om1val  22061  wlkntrl  25292  constr2trl  25329  constr2spth  25330  constr2pth  25331  2pthon  25332  2pthon3v  25334  usgra2adedgwlkon  25343  usg2wlk  25345  usg2wlkon  25346  constr3lem1  25373  constr3cyclpe  25391  3v3e3cycl2  25392  signswbase  29443  signswplusg  29444  ldualset  32691  erngset  34367  erngset-rN  34375  dvaset  34572  dvhset  34649  hlhilset  35505  rabren3dioph  35658  mendval  36049  rngcvalALTV  40016  ringcvalALTV  40062  lmod1zrnlvec  40340