Theorem tpex 7691

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 4585	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5382	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5381	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7689	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2832	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 2113  Vcvv 3440   ∪ cun 3899  {csn 4580  {cpr 4582  {ctp 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-sn 4581  df-pr 4583  df-tp 4585  df-uni 4864

This theorem is referenced by:  fr3nr  7717  en3lp  9523  prdsval  17375  imasval  17432  fnfuc  17872  fucval  17885  setcval  18001  catcval  18024  estrcval  18047  estrreslem1  18060  estrres  18062  fnxpc  18099  xpcval  18100  efmnd  18795  cnfldex  21312  xrsex  21339  psrval  21871  om1val  24986  rlocbas  33349  rlocaddval  33350  rlocmulval  33351  idlsrgval  33584  evl1deg2  33658  signswbase  34711  signswplusg  34712  ldualset  39381  erngset  41056  erngset-rN  41064  dvaset  41261  dvhset  41337  hlhilset  42190  rabren3dioph  43053  mendval  43417  clsk1indlem4  44281  clsk1indlem1  44282  grtrimap  48190  usgrgrtrirex  48192  grlimgrtri  48245  rngcvalALTV  48507  ringcvalALTV  48531  lmod1zrnlvec  48736  mndtcval  49820