Theorem tpex 7679

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436   ∪ cun 3900  {csn 4576  {cpr 4578  {ctp 4580

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370  ax-un 7668

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-sn 4577  df-pr 4579  df-tp 4581  df-uni 4860

This theorem is referenced by:  fr3nr  7705  en3lp  9504  prdsval  17356  imasval  17412  fnfuc  17852  fucval  17865  setcval  17981  catcval  18004  estrcval  18027  estrreslem1  18040  estrres  18042  fnxpc  18079  xpcval  18080  efmnd  18775  cnfldex  21292  xrsex  21319  psrval  21850  om1val  24955  rlocbas  33229  rlocaddval  33230  rlocmulval  33231  idlsrgval  33463  evl1deg2  33535  signswbase  34562  signswplusg  34563  ldualset  39163  erngset  40838  erngset-rN  40846  dvaset  41043  dvhset  41119  hlhilset  41972  rabren3dioph  42847  mendval  43211  clsk1indlem4  44076  clsk1indlem1  44077  grtrimap  47978  usgrgrtrirex  47980  grlimgrtri  48033  rngcvalALTV  48295  ringcvalALTV  48319  lmod1zrnlvec  48525  mndtcval  49610