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 4635
Description: Define unordered triple of classes. Definition of [Enderton] p. 19.

Note: ordered triples are a completely different object defined below in df-ot 4639. 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 4634 . 2 class {𝐴, 𝐵, 𝐶}
51, 2cpr 4632 . . 3 class {𝐴, 𝐵}
63csn 4630 . . 3 class {𝐶}
75, 6cun 3942 . 2 class ({𝐴, 𝐵} ∪ {𝐶})
84, 7wceq 1533 1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
Colors of variables: wff setvar class
This definition is referenced by:  eltpg  4691  raltpg  4704  rextpg  4705  disjtpsn  4721  disjtp2  4722  tpeq1  4748  tpeq2  4749  tpeq3  4750  tpcoma  4756  tpass  4758  qdass  4759  tpidm12  4761  diftpsn3  4807  tpprceq3  4809  tppreqb  4810  snsstp1  4821  snsstp2  4822  snsstp3  4823  sstp  4839  tpss  4840  tpssi  4841  ord3ex  5387  dmtpop  6224  funtpg  6609  funtp  6611  fntpg  6614  funcnvtp  6617  ftpg  7165  fvtp1  7207  fvtp1g  7210  tpex  7750  fr3nr  7775  tpfi  9349  fztp  13592  hashtplei  14481  hashtpg  14482  s3tpop  14896  sumtp  15731  bpoly3  16038  strle3  17132  estrreslem2  18132  estrres  18133  lsptpcl  20875  perfectlem2  27208  sltsolem1  27654  ex-un  30306  ex-ss  30309  ex-pw  30311  ex-hash  30335  fnimatp  32544  prodtp  32675  dvh4dimlem  41046  dvhdimlem  41047  dvh4dimN  41050  df3o2  42884  df3o3  42885  omcl3g  42905  onsucunitp  42944  oaun3  42953  tr3dom  43100  perfectALTVlem2  47199
  Copyright terms: Public domain W3C validator