Theorem tpex 7725

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450   ∪ cun 3915  {csn 4592  {cpr 4594  {ctp 4596

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-sn 4593  df-pr 4595  df-tp 4597  df-uni 4875

This theorem is referenced by:  fr3nr  7751  en3lp  9574  prdsval  17425  imasval  17481  fnfuc  17917  fucval  17930  setcval  18046  catcval  18069  estrcval  18092  estrreslem1  18105  estrres  18107  fnxpc  18144  xpcval  18145  efmnd  18804  cnfldex  21274  xrsex  21301  psrval  21831  om1val  24937  rlocbas  33225  rlocaddval  33226  rlocmulval  33227  idlsrgval  33481  evl1deg2  33553  signswbase  34552  signswplusg  34553  ldualset  39125  erngset  40801  erngset-rN  40809  dvaset  41006  dvhset  41082  hlhilset  41935  rabren3dioph  42810  mendval  43175  clsk1indlem4  44040  clsk1indlem1  44041  grtrimap  47951  usgrgrtrirex  47953  grlimgrtri  47999  rngcvalALTV  48257  ringcvalALTV  48281  lmod1zrnlvec  48487  mndtcval  49572