MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tp Unicode version

Definition df-tp 4034
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
2 cB . . 3
3 cC . . 3
41, 2, 3ctp 4033 . 2
51, 2cpr 4031 . . 3
63csn 4029 . . 3
75, 6cun 3473 . 2
84, 7wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  eltpg  4071  raltpg  4080  rextpg  4081  tpeq1  4118  tpeq2  4119  tpeq3  4120  tpcoma  4126  tpass  4128  qdass  4129  tpidm12  4131  diftpsn3  4168  tpprceq3  4170  tppreqb  4171  snsstp1  4181  snsstp2  4182  snsstp3  4183  sstp  4194  tpss  4195  tpssi  4196  ord3ex  4642  dmtpop  5489  funtpg  5643  funtp  5645  fntpg  5648  ftpg  6081  fvtp1  6118  fvtp1g  6121  tpex  6599  fr3nr  6615  tpfi  7816  fztp  11765  hashtplei  12522  hashtpg  12523  strlemor3  14726  strle3  14730  lsptpcl  17625  perfectlem2  23505  constr2spthlem1  24596  ex-un  25145  ex-ss  25148  ex-pw  25150  sltsolem1  29428  bpoly3  29820  estrreslem2  32644  estrres  32645  dvh4dimlem  37170  dvhdimlem  37171  dvh4dimN  37174
  Copyright terms: Public domain W3C validator