Theorem tpex 7765

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 4636	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5443	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5442	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7763	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2835	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3478   ∪ cun 3961  {csn 4631  {cpr 4633  {ctp 4635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-sn 4632  df-pr 4634  df-tp 4636  df-uni 4913

This theorem is referenced by:  fr3nr  7791  en3lp  9652  prdsval  17502  imasval  17558  fnfuc  18000  fucval  18014  setcval  18131  catcval  18154  estrcval  18179  estrreslem1  18192  estrreslem1OLD  18193  estrres  18195  fnxpc  18232  xpcval  18233  efmnd  18896  cnfldex  21385  xrsex  21413  psrval  21953  om1val  25077  rlocbas  33254  rlocaddval  33255  rlocmulval  33256  idlsrgval  33511  evl1deg2  33582  signswbase  34548  signswplusg  34549  ldualset  39107  erngset  40783  erngset-rN  40791  dvaset  40988  dvhset  41064  hlhilset  41917  rabren3dioph  42803  mendval  43168  clsk1indlem4  44034  clsk1indlem1  44035  grtrimap  47851  usgrgrtrirex  47853  grlimgrtri  47899  rngcvalALTV  48109  ringcvalALTV  48133  lmod1zrnlvec  48340  mndtcval  48888