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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451   ∪ cun 3897  {csn 4584  {cpr 4586  {ctp 4588

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 2733  ax-sep 5249  ax-pr 5391  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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-sn 4585  df-pr 4587  df-tp 4589  df-uni 4868

This theorem is used by:  fr3nr  7775  en3lp  9599  prdsval  17606  imasval  17663  fnfuc  18103  fucval  18116  setcval  18232  catcval  18255  estrcval  18278  estrreslem1  18291  estrres  18293  fnxpc  18330  xpcval  18331  efmnd  19046  degenmgmopdm  19114  degenmgm  19117  degenmgm2opdm  19118  degenmgm2nfun  19119  degenmgm2  19120  cnfldex  21661  xrsex  21675  psrval  22203  om1val  25331  angmgmlem  29377  angmgmbas  29380  rlocbas  33811  rlocaddval  33812  rlocmulval  33813  idlsrgval  34017  evl1deg2  34091  signswbase  35166  signswplusg  35167  ldualset  40150  erngset  41825  erngset-rN  41833  dvaset  42030  dvhset  42106  hlhilset  42959  rabren3dioph  43775  mendval  44139  clsk1indlem4  45003  clsk1indlem1  45004  grtrimap  48990  usgrgrtrirex  48992  grlimgrtri  49045  rngcvalALTV  49306  ringcvalALTV  49330  lmod1zrnlvec  49550  mndtcval  50631