Theorem tpex 7756

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 4599	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5414	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5415	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7755	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2862	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3458   ∪ cun 3906  {csn 4594  {cpr 4596  {ctp 4598

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 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409  ax-un 7745

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925  df-sn 4595  df-pr 4597  df-tp 4599  df-uni 4878

This theorem is used by:  fr3nr  7780  en3lp  9593  prdsval  17533  imasval  17590  fnfuc  18030  fucval  18043  setcval  18159  catcval  18182  estrcval  18205  estrreslem1  18218  estrres  18220  fnxpc  18257  xpcval  18258  efmnd  18960  cnfldex  21562  xrsex  21576  psrval  22102  om1val  25226  rlocbas  33619  rlocaddval  33620  rlocmulval  33621  idlsrgval  33824  evl1deg2  33898  signswbase  34973  signswplusg  34974  ldualset  39940  erngset  41615  erngset-rN  41623  dvaset  41820  dvhset  41896  hlhilset  42749  rabren3dioph  43583  mendval  43947  clsk1indlem4  44811  clsk1indlem1  44812  grtrimap  48754  usgrgrtrirex  48756  grlimgrtri  48809  rngcvalALTV  49071  ringcvalALTV  49095  lmod1zrnlvec  49315  mndtcval  50398