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 4160
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 4159 . 2 class {𝐴, 𝐵, 𝐶}
51, 2cpr 4157 . . 3 class {𝐴, 𝐵}
63csn 4155 . . 3 class {𝐶}
75, 6cun 3558 . 2 class ({𝐴, 𝐵} ∪ {𝐶})
84, 7wceq 1480 1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
Colors of variables: wff setvar class
This definition is referenced by:  eltpg  4205  raltpg  4214  rextpg  4215  disjtpsn  4228  disjtp2  4229  tpeq1  4254  tpeq2  4255  tpeq3  4256  tpcoma  4262  tpass  4264  qdass  4265  tpidm12  4267  diftpsn3  4308  diftpsn3OLD  4309  tpprceq3  4311  tppreqb  4312  snsstp1  4322  snsstp2  4323  snsstp3  4324  sstp  4342  tpss  4343  tpssi  4344  ord3ex  4826  dmtpop  5580  funtpg  5910  funtpgOLD  5911  funtp  5913  fntpg  5916  funcnvtp  5919  ftpg  6388  fvtp1  6425  fvtp1g  6428  tpex  6922  fr3nr  6941  tpfi  8196  fztp  12355  hashtplei  13220  hashtpg  13221  s3tpop  13606  sumtp  14427  bpoly3  14733  strlemor3OLD  15911  strle3  15915  estrreslem2  16718  estrres  16719  lsptpcl  18919  perfectlem2  24889  ex-un  27169  ex-ss  27172  ex-pw  27174  ex-hash  27198  sltsolem1  31581  dvh4dimlem  36251  dvhdimlem  36252  dvh4dimN  36255  df3o2  37843  df3o3  37844  perfectALTVlem2  40956
  Copyright terms: Public domain W3C validator