Theorem tpex 7722

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 4594	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5392	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5391	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7720	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2824	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3447   ∪ cun 3912  {csn 4589  {cpr 4591  {ctp 4593

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

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 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-sn 4590  df-pr 4592  df-tp 4594  df-uni 4872

This theorem is referenced by:  fr3nr  7748  en3lp  9567  prdsval  17418  imasval  17474  fnfuc  17910  fucval  17923  setcval  18039  catcval  18062  estrcval  18085  estrreslem1  18098  estrres  18100  fnxpc  18137  xpcval  18138  efmnd  18797  cnfldex  21267  xrsex  21294  psrval  21824  om1val  24930  rlocbas  33218  rlocaddval  33219  rlocmulval  33220  idlsrgval  33474  evl1deg2  33546  signswbase  34545  signswplusg  34546  ldualset  39118  erngset  40794  erngset-rN  40802  dvaset  40999  dvhset  41075  hlhilset  41928  rabren3dioph  42803  mendval  43168  clsk1indlem4  44033  clsk1indlem1  44034  grtrimap  47947  usgrgrtrirex  47949  grlimgrtri  47995  rngcvalALTV  48253  ringcvalALTV  48277  lmod1zrnlvec  48483  mndtcval  49568