Theorem tpex 7696

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

Assertion

Ref	Expression
tpex	⊢ {𝐴, 𝐵, 𝐶} ∈ V

Proof of Theorem tpex

Step	Hyp	Ref	Expression
1		df-tp 4567	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5374	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5375	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7694	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2836	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 2119  Vcvv 3432   ∪ cun 3888  {csn 4562  {cpr 4564  {ctp 4566

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907  df-sn 4563  df-pr 4565  df-tp 4567  df-uni 4846

This theorem is referenced by:  fr3nr  7722  en3lp  9533  prdsval  17416  imasval  17473  fnfuc  17913  fucval  17926  setcval  18042  catcval  18065  estrcval  18088  estrreslem1  18101  estrres  18103  fnxpc  18140  xpcval  18141  efmnd  18836  cnfldex  21357  xrsex  21371  psrval  21897  om1val  25022  rlocbas  33355  rlocaddval  33356  rlocmulval  33357  idlsrgval  33593  evl1deg2  33667  signswbase  34745  signswplusg  34746  ldualset  39624  erngset  41299  erngset-rN  41307  dvaset  41504  dvhset  41580  hlhilset  42433  rabren3dioph  43267  mendval  43631  clsk1indlem4  44495  clsk1indlem1  44496  grtrimap  48446  usgrgrtrirex  48448  grlimgrtri  48501  rngcvalALTV  48763  ringcvalALTV  48787  lmod1zrnlvec  48992  mndtcval  50076