Theorem tpex 7470

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 5333	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5332	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7469	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2909	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3494   ∪ cun 3934  {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 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-sn 4568  df-pr 4570  df-tp 4572  df-uni 4839

This theorem is referenced by:  fr3nr  7494  en3lp  9077  prdsval  16728  imasval  16784  fnfuc  17215  fucval  17228  setcval  17337  catcval  17356  estrcval  17374  estrreslem1  17387  estrres  17389  fnxpc  17426  xpcval  17427  efmnd  18035  psrval  20142  xrsex  20560  om1val  23634  signswbase  31824  signswplusg  31825  ldualset  36276  erngset  37951  erngset-rN  37959  dvaset  38156  dvhset  38232  hlhilset  39085  rabren3dioph  39432  mendval  39803  clsk1indlem4  40414  clsk1indlem1  40415  rngcvalALTV  44252  ringcvalALTV  44298  lmod1zrnlvec  44569