Theorem tpex 6911

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 4158	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 4875	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 4874	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 6910	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2700	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 1992  Vcvv 3191   ∪ cun 3558  {csn 4153  {cpr 4155  {ctp 4157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pr 4872  ax-un 6903

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-rex 2918  df-v 3193  df-dif 3563  df-un 3565  df-nul 3897  df-sn 4154  df-pr 4156  df-tp 4158  df-uni 4408

This theorem is referenced by:  fr3nr  6927  en3lp  8458  prdsval  16031  imasval  16087  fnfuc  16521  fucval  16534  setcval  16643  catcval  16662  estrcval  16680  estrreslem1  16693  estrres  16695  fnxpc  16732  xpcval  16733  symgval  17715  psrval  19276  xrsex  19675  om1val  22733  signswbase  30403  signswplusg  30404  ldualset  33878  erngset  35554  erngset-rN  35562  dvaset  35759  dvhset  35836  hlhilset  36692  rabren3dioph  36845  mendval  37220  clsk1indlem4  37810  clsk1indlem1  37811  rngcvalALTV  41222  ringcvalALTV  41268  lmod1zrnlvec  41545