Theorem tpex 7693

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430   ∪ cun 3888  {csn 4568  {cpr 4570  {ctp 4572

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 5231  ax-pr 5370  ax-un 7682

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 3432  df-un 3895  df-ss 3907  df-sn 4569  df-pr 4571  df-tp 4573  df-uni 4852

This theorem is referenced by:  fr3nr  7719  en3lp  9526  prdsval  17409  imasval  17466  fnfuc  17906  fucval  17919  setcval  18035  catcval  18058  estrcval  18081  estrreslem1  18094  estrres  18096  fnxpc  18133  xpcval  18134  efmnd  18829  cnfldex  21347  xrsex  21374  psrval  21905  om1val  25007  rlocbas  33343  rlocaddval  33344  rlocmulval  33345  idlsrgval  33578  evl1deg2  33652  signswbase  34714  signswplusg  34715  ldualset  39585  erngset  41260  erngset-rN  41268  dvaset  41465  dvhset  41541  hlhilset  42394  rabren3dioph  43261  mendval  43625  clsk1indlem4  44489  clsk1indlem1  44490  grtrimap  48436  usgrgrtrirex  48438  grlimgrtri  48491  rngcvalALTV  48753  ringcvalALTV  48777  lmod1zrnlvec  48982  mndtcval  50066