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 4215
Description: Define unordered triple of classes. Definition of [Enderton] p. 19. (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 4214 . 2 class {𝐴, 𝐵, 𝐶}
51, 2cpr 4212 . . 3 class {𝐴, 𝐵}
63csn 4210 . . 3 class {𝐶}
75, 6cun 3605 . 2 class ({𝐴, 𝐵} ∪ {𝐶})
84, 7wceq 1523 1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
Colors of variables: wff setvar class
This definition is referenced by:  eltpg  4259  raltpg  4268  rextpg  4269  disjtpsn  4283  disjtp2  4284  tpeq1  4309  tpeq2  4310  tpeq3  4311  tpcoma  4317  tpass  4319  qdass  4320  tpidm12  4322  diftpsn3  4364  diftpsn3OLD  4365  tpprceq3  4367  tppreqb  4368  snsstp1  4379  snsstp2  4380  snsstp3  4381  sstp  4399  tpss  4400  tpssi  4401  ord3ex  4886  dmtpop  5647  funtpg  5980  funtpgOLD  5981  funtp  5983  fntpg  5986  funcnvtp  5989  ftpg  6463  fvtp1  6501  fvtp1g  6504  tpex  6999  fr3nr  7021  tpfi  8277  fztp  12435  hashtplei  13304  hashtpg  13305  s3tpop  13700  sumtp  14522  bpoly3  14833  strlemor3OLD  16018  strle3  16022  estrreslem2  16825  estrres  16826  lsptpcl  19027  perfectlem2  25000  ex-un  27411  ex-ss  27414  ex-pw  27416  ex-hash  27440  prodtp  29701  sltsolem1  31951  dvh4dimlem  37049  dvhdimlem  37050  dvh4dimN  37053  df3o2  38639  df3o3  38640  perfectALTVlem2  41956
  Copyright terms: Public domain W3C validator