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 4129
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 4128 . 2 class {𝐴, 𝐵, 𝐶}
51, 2cpr 4126 . . 3 class {𝐴, 𝐵}
63csn 4124 . . 3 class {𝐶}
75, 6cun 3537 . 2 class ({𝐴, 𝐵} ∪ {𝐶})
84, 7wceq 1474 1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
Colors of variables: wff setvar class
This definition is referenced by:  eltpg  4173  raltpg  4182  rextpg  4183  tpeq1  4220  tpeq2  4221  tpeq3  4222  tpcoma  4228  tpass  4230  qdass  4231  tpidm12  4233  diftpsn3  4272  diftpsn3OLD  4273  tpprceq3  4275  tppreqb  4276  snsstp1  4286  snsstp2  4287  snsstp3  4288  sstp  4302  tpss  4303  tpssi  4304  ord3ex  4776  dmtpop  5514  funtpg  5841  funtpgOLD  5842  funtp  5844  fntpg  5847  funcnvtp  5850  ftpg  6305  fvtp1  6342  fvtp1g  6345  tpex  6832  fr3nr  6848  tpfi  8098  fztp  12224  hashtplei  13072  hashtpg  13073  s3tpop  13452  sumtp  14270  bpoly3  14576  strlemor3  15746  strle3  15750  estrreslem2  16549  estrres  16550  lsptpcl  18748  perfectlem2  24699  constr2spthlem1  25917  ex-un  26466  ex-ss  26469  ex-pw  26471  ex-hash  26495  sltsolem1  30860  dvh4dimlem  35533  dvhdimlem  35534  dvh4dimN  35537  df3o2  37125  df3o3  37126  perfectALTVlem2  39949
  Copyright terms: Public domain W3C validator