Theorem tpex 7733

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 4590	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
2		prex 5399	. . 3 ⊢ {𝐴, 𝐵} ∈ V
3		snex 5400	. . 3 ⊢ {𝐶} ∈ V
4	2, 3	unex 7731	. 2 ⊢ ({𝐴, 𝐵} ∪ {𝐶}) ∈ V
5	1, 4	eqeltri 2861	1 ⊢ {𝐴, 𝐵, 𝐶} ∈ V

Syntax hints:   ∈ wcel 2145  Vcvv 3457   ∪ cun 3905  {csn 4585  {cpr 4587  {ctp 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5250  ax-pr 5394  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924  df-sn 4586  df-pr 4588  df-tp 4590  df-uni 4868

This theorem is referenced by:  fr3nr  7759  en3lp  9571  prdsval  17496  imasval  17553  fnfuc  17993  fucval  18006  setcval  18122  catcval  18145  estrcval  18168  estrreslem1  18181  estrres  18183  fnxpc  18220  xpcval  18221  efmnd  18917  cnfldex  21482  xrsex  21496  psrval  22022  om1val  25146  rlocbas  33496  rlocaddval  33497  rlocmulval  33498  idlsrgval  33705  evl1deg2  33779  signswbase  34853  signswplusg  34854  ldualset  39756  erngset  41431  erngset-rN  41439  dvaset  41636  dvhset  41712  hlhilset  42565  rabren3dioph  43399  mendval  43763  clsk1indlem4  44627  clsk1indlem1  44628  grtrimap  48569  usgrgrtrirex  48571  grlimgrtri  48624  rngcvalALTV  48886  ringcvalALTV  48910  lmod1zrnlvec  49126  mndtcval  50209