Theorem tpex 7682

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 4582	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5376	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5375	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7680	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2824	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3436   ∪ cun 3901  {csn 4577  {cpr 4579  {ctp 4581

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-sn 4578  df-pr 4580  df-tp 4582  df-uni 4859

This theorem is referenced by:  fr3nr  7708  en3lp  9510  prdsval  17359  imasval  17415  fnfuc  17855  fucval  17868  setcval  17984  catcval  18007  estrcval  18030  estrreslem1  18043  estrres  18045  fnxpc  18082  xpcval  18083  efmnd  18744  cnfldex  21264  xrsex  21291  psrval  21822  om1val  24928  rlocbas  33208  rlocaddval  33209  rlocmulval  33210  idlsrgval  33441  evl1deg2  33513  signswbase  34528  signswplusg  34529  ldualset  39114  erngset  40789  erngset-rN  40797  dvaset  40994  dvhset  41070  hlhilset  41923  rabren3dioph  42798  mendval  43162  clsk1indlem4  44027  clsk1indlem1  44028  grtrimap  47942  usgrgrtrirex  47944  grlimgrtri  47997  rngcvalALTV  48259  ringcvalALTV  48283  lmod1zrnlvec  48489  mndtcval  49574