Theorem tpex 7733

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 4590	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5400	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5401	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7731	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2861	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 2145  Vcvv 3457   ∪ cun 3905  {csn 4585  {cpr 4587  {ctp 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924  df-sn 4586  df-pr 4588  df-tp 4590  df-uni 4869

This theorem is referenced by:  fr3nr  7759  en3lp  9571  prdsval  17498  imasval  17555  fnfuc  17995  fucval  18008  setcval  18124  catcval  18147  estrcval  18170  estrreslem1  18183  estrres  18185  fnxpc  18222  xpcval  18223  efmnd  18919  cnfldex  21485  xrsex  21499  psrval  22025  om1val  25150  rlocbas  33501  rlocaddval  33502  rlocmulval  33503  idlsrgval  33710  evl1deg2  33784  signswbase  34858  signswplusg  34859  ldualset  39761  erngset  41436  erngset-rN  41444  dvaset  41641  dvhset  41717  hlhilset  42570  rabren3dioph  43404  mendval  43768  clsk1indlem4  44632  clsk1indlem1  44633  grtrimap  48568  usgrgrtrirex  48570  grlimgrtri  48623  rngcvalALTV  48885  ringcvalALTV  48909  lmod1zrnlvec  49125  mndtcval  50208