Theorem tpex 7781

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 4653	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5452	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5451	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7779	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2840	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3488   ∪ cun 3974  {csn 4648  {cpr 4650  {ctp 4652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-sn 4649  df-pr 4651  df-tp 4653  df-uni 4932

This theorem is referenced by:  fr3nr  7807  en3lp  9683  prdsval  17515  imasval  17571  fnfuc  18013  fucval  18027  setcval  18144  catcval  18167  estrcval  18192  estrreslem1  18205  estrreslem1OLD  18206  estrres  18208  fnxpc  18245  xpcval  18246  efmnd  18905  cnfldex  21390  xrsex  21418  psrval  21958  om1val  25082  rlocbas  33239  rlocaddval  33240  rlocmulval  33241  idlsrgval  33496  evl1deg2  33567  signswbase  34531  signswplusg  34532  ldualset  39081  erngset  40757  erngset-rN  40765  dvaset  40962  dvhset  41038  hlhilset  41891  rabren3dioph  42771  mendval  43140  clsk1indlem4  44006  clsk1indlem1  44007  grtrimap  47797  usgrgrtrirex  47799  grlimgrtri  47820  rngcvalALTV  47988  ringcvalALTV  48012  lmod1zrnlvec  48223  mndtcval  48752