Theorem tpex 7700

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 4572	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5380	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5381	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7698	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2832	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3429   ∪ cun 3887  {csn 4567  {cpr 4569  {ctp 4571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-sn 4568  df-pr 4570  df-tp 4572  df-uni 4851

This theorem is referenced by:  fr3nr  7726  en3lp  9535  prdsval  17418  imasval  17475  fnfuc  17915  fucval  17928  setcval  18044  catcval  18067  estrcval  18090  estrreslem1  18103  estrres  18105  fnxpc  18142  xpcval  18143  efmnd  18838  cnfldex  21355  xrsex  21369  psrval  21895  om1val  24997  rlocbas  33328  rlocaddval  33329  rlocmulval  33330  idlsrgval  33563  evl1deg2  33637  signswbase  34698  signswplusg  34699  ldualset  39571  erngset  41246  erngset-rN  41254  dvaset  41451  dvhset  41527  hlhilset  42380  rabren3dioph  43243  mendval  43607  clsk1indlem4  44471  clsk1indlem1  44472  grtrimap  48424  usgrgrtrirex  48426  grlimgrtri  48479  rngcvalALTV  48741  ringcvalALTV  48765  lmod1zrnlvec  48970  mndtcval  50054