Theorem tpex 6384

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 3887	. 2 |- { A , B , C } = ( { A , B } u. { C } )
2		prex 4539	. . 3 |- { A , B } e. _V
3		snex 4538	. . 3 |- { C } e. _V
4	2, 3	unex 6383	. 2 |- ( { A , B } u. { C } ) e. _V
5	1, 4	eqeltri 2513	1 |- { A , B , C } e. _V

Syntax hints:   e. wcel 1756   _Vcvv 2977   u. cun 3331   {csn 3882   {cpr 3884   {ctp 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pr 4536  ax-un 6377

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-rex 2726  df-v 2979  df-dif 3336  df-un 3338  df-nul 3643  df-sn 3883  df-pr 3885  df-tp 3887  df-uni 4097

This theorem is referenced by:  fr3nr  6396  en3lp  7827  prdsval  14398  imasval  14454  fnfuc  14860  fucval  14873  setcval  14950  catcval  14969  fnxpc  14991  xpcval  14992  symgval  15889  psrval  17434  xrsex  17836  om1val  20607  wlkntrl  23466  constr2wlk  23502  constr2trl  23503  constr2spth  23504  constr2pth  23505  2pthon  23506  2pthon3v  23508  constr3lem1  23536  constr3cyclpe  23554  3v3e3cycl2  23555  signswbase  26960  signswplusg  26961  rabren3dioph  29159  mendval  29545  usgra2adedgwlkon  30312  usg2wlk  30314  usg2wlkon  30315  lmod1zrnlvec  31041  ldualset  32775  erngset  34449  erngset-rN  34457  dvaset  34654  dvhset  34731  hlhilset  35587