Theorem tpex 7730

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 4632	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5431	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5430	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7729	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2829	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3474   ∪ cun 3945  {csn 4627  {cpr 4629  {ctp 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-sn 4628  df-pr 4630  df-tp 4632  df-uni 4908

This theorem is referenced by:  fr3nr  7755  en3lp  9605  prdsval  17397  imasval  17453  fnfuc  17892  fucval  17906  setcval  18023  catcval  18046  estrcval  18071  estrreslem1  18084  estrreslem1OLD  18085  estrres  18087  fnxpc  18124  xpcval  18125  efmnd  18747  xrsex  20952  psrval  21459  om1val  24537  idlsrgval  32605  signswbase  33553  signswplusg  33554  gg-cnfldex  35168  ldualset  37983  erngset  39659  erngset-rN  39667  dvaset  39864  dvhset  39940  hlhilset  40793  rabren3dioph  41538  mendval  41910  clsk1indlem4  42780  clsk1indlem1  42781  rngcvalALTV  46812  ringcvalALTV  46858  lmod1zrnlvec  47128  mndtcval  47658