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

Definition df-tp 4021
Description: Define unordered triple of classes. Definition of [Enderton] p. 19. (Contributed by NM, 9-Apr-1994.)
Assertion
Ref Expression
df-tp  |-  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )

Detailed syntax breakdown of Definition df-tp
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cC . . 3  class  C
41, 2, 3ctp 4020 . 2  class  { A ,  B ,  C }
51, 2cpr 4018 . . 3  class  { A ,  B }
63csn 4016 . . 3  class  { C }
75, 6cun 3459 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1398 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff setvar class
This definition is referenced by:  eltpg  4058  raltpg  4067  rextpg  4068  tpeq1  4104  tpeq2  4105  tpeq3  4106  tpcoma  4112  tpass  4114  qdass  4115  tpidm12  4117  diftpsn3  4154  tpprceq3  4156  tppreqb  4157  snsstp1  4167  snsstp2  4168  snsstp3  4169  sstp  4180  tpss  4181  tpssi  4182  ord3ex  4627  dmtpop  5467  funtpg  5620  funtp  5622  fntpg  5625  ftpg  6057  fvtp1  6094  fvtp1g  6097  tpex  6572  fr3nr  6588  tpfi  7788  fztp  11740  hashtplei  12506  hashtpg  12507  strlemor3  14813  strle3  14817  estrreslem2  15606  estrres  15607  lsptpcl  17820  perfectlem2  23703  constr2spthlem1  24798  ex-un  25347  ex-ss  25350  ex-pw  25352  sltsolem1  29668  bpoly3  30048  dvh4dimlem  37567  dvhdimlem  37568  dvh4dimN  37571
  Copyright terms: Public domain W3C validator