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 4564
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 4563 . 2 class {𝐴, 𝐵, 𝐶}
51, 2cpr 4561 . . 3 class {𝐴, 𝐵}
63csn 4559 . . 3 class {𝐶}
75, 6cun 3933 . 2 class ({𝐴, 𝐵} ∪ {𝐶})
84, 7wceq 1528 1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
Colors of variables: wff setvar class
This definition is referenced by:  eltpg  4617  raltpg  4628  rextpg  4629  disjtpsn  4645  disjtp2  4646  tpeq1  4672  tpeq2  4673  tpeq3  4674  tpcoma  4680  tpass  4682  qdass  4683  tpidm12  4685  diftpsn3  4729  tpprceq3  4731  tppreqb  4732  snsstp1  4743  snsstp2  4744  snsstp3  4745  sstp  4761  tpss  4762  tpssi  4763  ord3ex  5279  dmtpop  6069  funtpg  6403  funtp  6405  fntpg  6408  funcnvtp  6411  ftpg  6911  fvtp1  6950  fvtp1g  6953  tpex  7458  fr3nr  7482  tpfi  8783  fztp  12953  hashtplei  13832  hashtpg  13833  s3tpop  14261  sumtp  15094  bpoly3  15402  strle3  16584  estrreslem2  17378  estrres  17379  lsptpcl  19682  perfectlem2  25734  ex-un  28131  ex-ss  28134  ex-pw  28136  ex-hash  28160  fnimatp  30352  prodtp  30471  sltsolem1  33078  dvh4dimlem  38461  dvhdimlem  38462  dvh4dimN  38465  tr3dom  39774  df3o2  40254  df3o3  40255  perfectALTVlem2  43734
  Copyright terms: Public domain W3C validator