Theorem tpex 7740

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 4606	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5407	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5406	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7738	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2830	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3459   ∪ cun 3924  {csn 4601  {cpr 4603  {ctp 4605

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 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7729

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-sn 4602  df-pr 4604  df-tp 4606  df-uni 4884

This theorem is referenced by:  fr3nr  7766  en3lp  9628  prdsval  17469  imasval  17525  fnfuc  17961  fucval  17974  setcval  18090  catcval  18113  estrcval  18136  estrreslem1  18149  estrres  18151  fnxpc  18188  xpcval  18189  efmnd  18848  cnfldex  21318  xrsex  21345  psrval  21875  om1val  24981  rlocbas  33262  rlocaddval  33263  rlocmulval  33264  idlsrgval  33518  evl1deg2  33590  signswbase  34586  signswplusg  34587  ldualset  39143  erngset  40819  erngset-rN  40827  dvaset  41024  dvhset  41100  hlhilset  41953  rabren3dioph  42838  mendval  43203  clsk1indlem4  44068  clsk1indlem1  44069  grtrimap  47960  usgrgrtrirex  47962  grlimgrtri  48008  rngcvalALTV  48240  ringcvalALTV  48264  lmod1zrnlvec  48470  mndtcval  49456