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

Definition df-tp 3998
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 3997 . 2
51, 2cpr 3995 . . 3
63csn 3993 . . 3
75, 6cun 3440 . 2
84, 7wceq 1370 1
Colors of variables: wff setvar class
This definition is referenced by:  eltpg  4035  raltpg  4044  rextpg  4045  tpeq1  4080  tpeq2  4081  tpeq3  4082  tpcoma  4088  tpass  4090  qdass  4091  tpidm12  4093  diftpsn3  4129  tpprceq3  4130  tppreqb  4131  snsstp1  4141  snsstp2  4142  snsstp3  4143  sstp  4154  tpss  4155  tpssi  4156  ord3ex  4599  dmtpop  5434  funtpg  5587  funtp  5589  fntpg  5592  ftpg  6016  fvtp1  6050  fvtp1g  6053  tpex  6512  fr3nr  6524  tpfi  7722  fztp  11657  hashtplei  12343  hashtpg  12344  strlemor3  14426  strle3  14430  lsptpcl  17236  perfectlem2  22969  constr2spthlem1  23962  ex-un  24100  ex-ss  24103  ex-pw  24105  sltsolem1  28265  bpoly3  28657  dvh4dimlem  35939  dvhdimlem  35940  dvh4dimN  35943
  Copyright terms: Public domain W3C validator