Theorem tpex 6957

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 4182	. 2 |- { A , B , C } = ( { A , B } u. { C } )
2		prex 4909	. . 3 |- { A , B } e. _V
3		snex 4908	. . 3 |- { C } e. _V
4	2, 3	unex 6956	. 2 |- ( { A , B } u. { C } ) e. _V
5	1, 4	eqeltri 2697	1 |- { A , B , C } e. _V

Syntax hints:   e. wcel 1990   _Vcvv 3200   u. cun 3572   {csn 4177   {cpr 4179   {ctp 4181

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-v 3202  df-dif 3577  df-un 3579  df-nul 3916  df-sn 4178  df-pr 4180  df-tp 4182  df-uni 4437

This theorem is referenced by:  fr3nr  6979  en3lp  8513  prdsval  16115  imasval  16171  fnfuc  16605  fucval  16618  setcval  16727  catcval  16746  estrcval  16764  estrreslem1  16777  estrres  16779  fnxpc  16816  xpcval  16817  symgval  17799  psrval  19362  xrsex  19761  om1val  22830  signswbase  30631  signswplusg  30632  ldualset  34412  erngset  36088  erngset-rN  36096  dvaset  36293  dvhset  36370  hlhilset  37226  rabren3dioph  37379  mendval  37753  clsk1indlem4  38342  clsk1indlem1  38343  rngcvalALTV  41961  ringcvalALTV  42007  lmod1zrnlvec  42283