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 4130
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 4129 . 2 class {𝐴, 𝐵, 𝐶}
51, 2cpr 4127 . . 3 class {𝐴, 𝐵}
63csn 4125 . . 3 class {𝐶}
75, 6cun 3538 . 2 class ({𝐴, 𝐵} ∪ {𝐶})
84, 7wceq 1475 1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
Colors of variables: wff setvar class
This definition is referenced by:  eltpg  4174  raltpg  4183  rextpg  4184  tpeq1  4221  tpeq2  4222  tpeq3  4223  tpcoma  4229  tpass  4231  qdass  4232  tpidm12  4234  diftpsn3  4273  diftpsn3OLD  4274  tpprceq3  4276  tppreqb  4277  snsstp1  4287  snsstp2  4288  snsstp3  4289  sstp  4307  tpss  4308  tpssi  4309  ord3ex  4782  dmtpop  5529  funtpg  5856  funtpgOLD  5857  funtp  5859  fntpg  5862  funcnvtp  5865  ftpg  6328  fvtp1  6365  fvtp1g  6368  tpex  6855  fr3nr  6871  tpfi  8121  fztp  12267  hashtplei  13120  hashtpg  13121  s3tpop  13504  sumtp  14322  bpoly3  14628  strlemor3  15798  strle3  15802  estrreslem2  16601  estrres  16602  lsptpcl  18800  perfectlem2  24755  constr2spthlem1  26124  ex-un  26673  ex-ss  26676  ex-pw  26678  ex-hash  26702  sltsolem1  31067  dvh4dimlem  35750  dvhdimlem  35751  dvh4dimN  35754  df3o2  37342  df3o3  37343  perfectALTVlem2  40165
  Copyright terms: Public domain W3C validator