Theorem tpex 7786

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454   ∪ cun 4152  {csn 4588  {cpr 4590  {ctp 4592

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395  ax-un 7775

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-sn 4589  df-pr 4591  df-tp 4593  df-uni 4871

This theorem is used by:  fr3nr  7810  en3lp  9642  prdsval  17655  imasval  17712  fnfuc  18152  fucval  18165  setcval  18281  catcval  18304  estrcval  18327  estrreslem1  18340  estrres  18342  fnxpc  18379  xpcval  18380  efmnd  19095  degenmgmopdm  19163  degenmgm  19166  degenmgm2opdm  19167  degenmgm2nfun  19168  degenmgm2  19169  cnfldex  21711  xrsex  21725  psrval  22253  om1val  25381  angmgmlem  29425  angmgmbas  29428  rlocbas  33899  rlocaddval  33900  rlocmulval  33901  idlsrgval  34105  evl1deg2  34179  signswbase  35253  signswplusg  35254  ldualset  40374  erngset  42049  erngset-rN  42057  dvaset  42254  dvhset  42330  hlhilset  43183  rabren3dioph  44015  mendval  44373  clsk1indlem4  45236  clsk1indlem1  45237  grtrimap  49251  usgrgrtrirex  49253  grlimgrtri  49306  rngcvalALTV  49567  ringcvalALTV  49591  lmod1zrnlvec  49811  mndtcval  50922  parcatid2  50968  parcatid  50969