Theorem tpex 7751

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453   ∪ cun 3900  {csn 4587  {cpr 4589  {ctp 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919  df-sn 4588  df-pr 4590  df-tp 4592  df-uni 4871

This theorem is used by:  fr3nr  7775  en3lp  9597  prdsval  17546  imasval  17603  fnfuc  18043  fucval  18056  setcval  18172  catcval  18195  estrcval  18218  estrreslem1  18231  estrres  18233  fnxpc  18270  xpcval  18271  efmnd  18985  degenmgmopdm  19053  degenmgm  19056  degenmgm2opdm  19057  degenmgm2nfun  19058  degenmgm2  19059  cnfldex  21594  xrsex  21608  psrval  22136  om1val  25264  angmgmlem  29282  angmgmbas  29285  rlocbas  33716  rlocaddval  33717  rlocmulval  33718  idlsrgval  33921  evl1deg2  33995  signswbase  35070  signswplusg  35071  ldualset  40006  erngset  41681  erngset-rN  41689  dvaset  41886  dvhset  41962  hlhilset  42815  rabren3dioph  43664  mendval  44028  clsk1indlem4  44892  clsk1indlem1  44893  grtrimap  48872  usgrgrtrirex  48874  grlimgrtri  48927  rngcvalALTV  49188  ringcvalALTV  49212  lmod1zrnlvec  49432  mndtcval  50513