MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tp Structured version   Visualization version   GIF version

Definition df-tp 4555
Description: Define unordered triple of classes. Definition of [Enderton] p. 19.

Note: ordered triples are a completely different object defined below in df-ot 4559. As with all tuples, when the term "triple" is used without qualifier, it means "ordered triple". (Contributed by NM, 9-Apr-1994.)

Assertion
Ref Expression
df-tp {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})

Detailed syntax breakdown of Definition df-tp
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cC . . 3 class 𝐶
41, 2, 3ctp 4554 . 2 class {𝐴, 𝐵, 𝐶}
51, 2cpr 4552 . . 3 class {𝐴, 𝐵}
63csn 4550 . . 3 class {𝐶}
75, 6cun 3917 . 2 class ({𝐴, 𝐵} ∪ {𝐶})
84, 7wceq 1538 1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
Colors of variables: wff setvar class
This definition is referenced by:  eltpg  4608  raltpg  4619  rextpg  4620  disjtpsn  4636  disjtp2  4637  tpeq1  4663  tpeq2  4664  tpeq3  4665  tpcoma  4671  tpass  4673  qdass  4674  tpidm12  4676  diftpsn3  4719  tpprceq3  4721  tppreqb  4722  snsstp1  4733  snsstp2  4734  snsstp3  4735  sstp  4751  tpss  4752  tpssi  4753  ord3ex  5276  dmtpop  6064  funtpg  6399  funtp  6401  fntpg  6404  funcnvtp  6407  ftpg  6911  fvtp1  6950  fvtp1g  6953  tpex  7466  fr3nr  7490  tpfi  8793  fztp  12969  hashtplei  13849  hashtpg  13850  s3tpop  14273  sumtp  15106  bpoly3  15414  strle3  16596  estrreslem2  17390  estrres  17391  lsptpcl  19753  perfectlem2  25823  ex-un  28218  ex-ss  28221  ex-pw  28223  ex-hash  28247  fnimatp  30442  prodtp  30564  sltsolem1  33265  dvh4dimlem  38711  dvhdimlem  38712  dvh4dimN  38715  tr3dom  40180  df3o2  40674  df3o3  40675  perfectALTVlem2  44193
  Copyright terms: Public domain W3C validator