Theorem tpex 7473

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 4575	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5336	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5335	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7472	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2912	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 2113  Vcvv 3497   ∪ cun 3937  {csn 4570  {cpr 4572  {ctp 4574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pr 5333  ax-un 7464

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-sn 4571  df-pr 4573  df-tp 4575  df-uni 4842

This theorem is referenced by:  fr3nr  7497  en3lp  9080  prdsval  16731  imasval  16787  fnfuc  17218  fucval  17231  setcval  17340  catcval  17359  estrcval  17377  estrreslem1  17390  estrres  17392  fnxpc  17429  xpcval  17430  efmnd  18038  psrval  20145  xrsex  20563  om1val  23637  signswbase  31828  signswplusg  31829  ldualset  36265  erngset  37940  erngset-rN  37948  dvaset  38145  dvhset  38221  hlhilset  39074  rabren3dioph  39418  mendval  39789  clsk1indlem4  40400  clsk1indlem1  40401  rngcvalALTV  44239  ringcvalALTV  44285  lmod1zrnlvec  44556