MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tp Structured version   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  |-  { 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 3997 . 2  class  { A ,  B ,  C }
51, 2cpr 3995 . . 3  class  { A ,  B }
63csn 3993 . . 3  class  { C }
75, 6cun 3431 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1437 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff setvar class
This definition is referenced by:  eltpg  4036  raltpg  4045  rextpg  4046  tpeq1  4082  tpeq2  4083  tpeq3  4084  tpcoma  4090  tpass  4092  qdass  4093  tpidm12  4095  diftpsn3  4132  tpprceq3  4134  tppreqb  4135  snsstp1  4145  snsstp2  4146  snsstp3  4147  sstp  4158  tpss  4159  tpssi  4160  ord3ex  4606  dmtpop  5323  funtpg  5642  funtp  5644  fntpg  5647  ftpg  6080  fvtp1  6117  fvtp1g  6120  tpex  6595  fr3nr  6611  tpfi  7844  fztp  11839  hashtplei  12620  hashtpg  12621  sumtp  13777  bpoly3  14078  strlemor3  15171  strle3  15175  estrreslem2  15967  estrres  15968  lsptpcl  18130  perfectlem2  24018  constr2spthlem1  25166  ex-un  25716  ex-ss  25719  ex-pw  25721  sltsolem1  30339  dvh4dimlem  34720  dvhdimlem  34721  dvh4dimN  34724  perfectALTVlem2  38247
  Copyright terms: Public domain W3C validator