Theorem tpex 7736

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

Syntax hints:   ∈ wcel 2106  Vcvv 3474   ∪ cun 3946  {csn 4628  {cpr 4630  {ctp 4632

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 5299  ax-nul 5306  ax-pr 5427  ax-un 7727

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 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-sn 4629  df-pr 4631  df-tp 4633  df-uni 4909

This theorem is referenced by:  fr3nr  7761  en3lp  9611  prdsval  17403  imasval  17459  fnfuc  17898  fucval  17912  setcval  18029  catcval  18052  estrcval  18077  estrreslem1  18090  estrreslem1OLD  18091  estrres  18093  fnxpc  18130  xpcval  18131  efmnd  18753  xrsex  20966  psrval  21474  om1val  24553  idlsrgval  32662  signswbase  33634  signswplusg  33635  gg-cnfldex  35255  ldualset  38087  erngset  39763  erngset-rN  39771  dvaset  39968  dvhset  40044  hlhilset  40897  rabren3dioph  41641  mendval  42013  clsk1indlem4  42883  clsk1indlem1  42884  rngcvalALTV  46944  ringcvalALTV  46990  lmod1zrnlvec  47259  mndtcval  47789