Theorem tpex 7575

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 4563	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5350	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5349	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7574	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2835	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3422   ∪ cun 3881  {csn 4558  {cpr 4560  {ctp 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-sn 4559  df-pr 4561  df-tp 4563  df-uni 4837

This theorem is referenced by:  fr3nr  7600  en3lp  9302  prdsval  17083  imasval  17139  fnfuc  17577  fucval  17591  setcval  17708  catcval  17731  estrcval  17756  estrreslem1  17769  estrreslem1OLD  17770  estrres  17772  fnxpc  17809  xpcval  17810  efmnd  18424  xrsex  20525  psrval  21028  om1val  24099  idlsrgval  31550  signswbase  32433  signswplusg  32434  ldualset  37066  erngset  38741  erngset-rN  38749  dvaset  38946  dvhset  39022  hlhilset  39875  rabren3dioph  40553  mendval  40924  clsk1indlem4  41543  clsk1indlem1  41544  rngcvalALTV  45407  ringcvalALTV  45453  lmod1zrnlvec  45723  mndtcval  46252