Theorem tpex 7474

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 4530	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5305	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5304	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7473	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2848	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 2111  Vcvv 3409   ∪ cun 3858  {csn 4525  {cpr 4527  {ctp 4529

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pr 5302  ax-un 7465

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-sn 4526  df-pr 4528  df-tp 4530  df-uni 4802

This theorem is referenced by:  fr3nr  7499  en3lp  9123  prdsval  16800  imasval  16856  fnfuc  17288  fucval  17301  setcval  17417  catcval  17436  estrcval  17454  estrreslem1  17467  estrres  17469  fnxpc  17506  xpcval  17507  efmnd  18115  xrsex  20195  psrval  20691  om1val  23745  idlsrgval  31182  signswbase  32065  signswplusg  32066  ldualset  36736  erngset  38411  erngset-rN  38419  dvaset  38616  dvhset  38692  hlhilset  39545  rabren3dioph  40174  mendval  40545  clsk1indlem4  41165  clsk1indlem1  41166  rngcvalALTV  45011  ringcvalALTV  45057  lmod1zrnlvec  45327