Theorem tpex 7746

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 4595	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5411	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5412	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7744	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2859	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 2143  Vcvv 3455   ∪ cun 3904  {csn 4590  {cpr 4592  {ctp 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923  df-sn 4591  df-pr 4593  df-tp 4595  df-uni 4874

This theorem is referenced by:  fr3nr  7772  en3lp  9584  prdsval  17509  imasval  17566  fnfuc  18006  fucval  18019  setcval  18135  catcval  18158  estrcval  18181  estrreslem1  18194  estrres  18196  fnxpc  18233  xpcval  18234  efmnd  18930  cnfldex  21506  xrsex  21520  psrval  22046  om1val  25170  rlocbas  33566  rlocaddval  33567  rlocmulval  33568  idlsrgval  33771  evl1deg2  33845  signswbase  34919  signswplusg  34920  ldualset  39877  erngset  41552  erngset-rN  41560  dvaset  41757  dvhset  41833  hlhilset  42686  rabren3dioph  43522  mendval  43886  clsk1indlem4  44750  clsk1indlem1  44751  grtrimap  48690  usgrgrtrirex  48692  grlimgrtri  48745  rngcvalALTV  49007  ringcvalALTV  49031  lmod1zrnlvec  49251  mndtcval  50334