Theorem tpex 7701

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 4587	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5384	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5385	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7699	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2833	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3442   ∪ cun 3901  {csn 4582  {cpr 4584  {ctp 4586

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-sn 4583  df-pr 4585  df-tp 4587  df-uni 4866

This theorem is referenced by:  fr3nr  7727  en3lp  9535  prdsval  17387  imasval  17444  fnfuc  17884  fucval  17897  setcval  18013  catcval  18036  estrcval  18059  estrreslem1  18072  estrres  18074  fnxpc  18111  xpcval  18112  efmnd  18807  cnfldex  21324  xrsex  21351  psrval  21883  om1val  24998  rlocbas  33360  rlocaddval  33361  rlocmulval  33362  idlsrgval  33595  evl1deg2  33669  signswbase  34731  signswplusg  34732  ldualset  39495  erngset  41170  erngset-rN  41178  dvaset  41375  dvhset  41451  hlhilset  42304  rabren3dioph  43166  mendval  43530  clsk1indlem4  44394  clsk1indlem1  44395  grtrimap  48302  usgrgrtrirex  48304  grlimgrtri  48357  rngcvalALTV  48619  ringcvalALTV  48643  lmod1zrnlvec  48848  mndtcval  49932