Theorem tpex 7766

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 4631	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5437	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5436	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7764	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2837	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3480   ∪ cun 3949  {csn 4626  {cpr 4628  {ctp 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-sn 4627  df-pr 4629  df-tp 4631  df-uni 4908

This theorem is referenced by:  fr3nr  7792  en3lp  9654  prdsval  17500  imasval  17556  fnfuc  17993  fucval  18006  setcval  18122  catcval  18145  estrcval  18168  estrreslem1  18181  estrreslem1OLD  18182  estrres  18184  fnxpc  18221  xpcval  18222  efmnd  18883  cnfldex  21367  xrsex  21395  psrval  21935  om1val  25063  rlocbas  33271  rlocaddval  33272  rlocmulval  33273  idlsrgval  33531  evl1deg2  33602  signswbase  34569  signswplusg  34570  ldualset  39126  erngset  40802  erngset-rN  40810  dvaset  41007  dvhset  41083  hlhilset  41936  rabren3dioph  42826  mendval  43191  clsk1indlem4  44057  clsk1indlem1  44058  grtrimap  47915  usgrgrtrirex  47917  grlimgrtri  47963  rngcvalALTV  48181  ringcvalALTV  48205  lmod1zrnlvec  48411  mndtcval  49176