Theorem tpex 7762

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 4589	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5395	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5396	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7761	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2856	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450   ∪ cun 4149  {csn 4584  {cpr 4586  {ctp 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151  df-sn 4585  df-pr 4587  df-tp 4589  df-uni 4867

This theorem is used by:  fr3nr  7786  en3lp  9618  prdsval  17631  imasval  17688  fnfuc  18128  fucval  18141  setcval  18257  catcval  18280  estrcval  18303  estrreslem1  18316  estrres  18318  fnxpc  18355  xpcval  18356  efmnd  19071  degenmgmopdm  19139  degenmgm  19142  degenmgm2opdm  19143  degenmgm2nfun  19144  degenmgm2  19145  cnfldex  21686  xrsex  21700  psrval  22228  om1val  25356  angmgmlem  29400  angmgmbas  29403  rlocbas  33875  rlocaddval  33876  rlocmulval  33877  idlsrgval  34081  evl1deg2  34155  signswbase  35229  signswplusg  35230  ldualset  40275  erngset  41950  erngset-rN  41958  dvaset  42155  dvhset  42231  hlhilset  43084  rabren3dioph  43915  mendval  44274  clsk1indlem4  45137  clsk1indlem1  45138  grtrimap  49139  usgrgrtrirex  49141  grlimgrtri  49194  rngcvalALTV  49455  ringcvalALTV  49479  lmod1zrnlvec  49699  mndtcval  50810  parcatid2  50856  parcatid  50857