Theorem tpex 7597

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

Syntax hints:   ∈ wcel 2106  Vcvv 3432   ∪ cun 3885  {csn 4561  {cpr 4563  {ctp 4565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-sn 4562  df-pr 4564  df-tp 4566  df-uni 4840

This theorem is referenced by:  fr3nr  7622  en3lp  9372  prdsval  17166  imasval  17222  fnfuc  17661  fucval  17675  setcval  17792  catcval  17815  estrcval  17840  estrreslem1  17853  estrreslem1OLD  17854  estrres  17856  fnxpc  17893  xpcval  17894  efmnd  18509  xrsex  20613  psrval  21118  om1val  24193  idlsrgval  31648  signswbase  32533  signswplusg  32534  ldualset  37139  erngset  38814  erngset-rN  38822  dvaset  39019  dvhset  39095  hlhilset  39948  rabren3dioph  40637  mendval  41008  clsk1indlem4  41654  clsk1indlem1  41655  rngcvalALTV  45519  ringcvalALTV  45565  lmod1zrnlvec  45835  mndtcval  46366