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

Definition df-tp 4016
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 4015 . 2  class  { A ,  B ,  C }
51, 2cpr 4013 . . 3  class  { A ,  B }
63csn 4011 . . 3  class  { C }
75, 6cun 3457 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1381 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff setvar class
This definition is referenced by:  eltpg  4053  raltpg  4062  rextpg  4063  tpeq1  4100  tpeq2  4101  tpeq3  4102  tpcoma  4108  tpass  4110  qdass  4111  tpidm12  4113  diftpsn3  4150  tpprceq3  4152  tppreqb  4153  snsstp1  4163  snsstp2  4164  snsstp3  4165  sstp  4176  tpss  4177  tpssi  4178  ord3ex  4624  dmtpop  5471  funtpg  5625  funtp  5627  fntpg  5630  ftpg  6063  fvtp1  6100  fvtp1g  6103  tpex  6581  fr3nr  6597  tpfi  7795  fztp  11742  hashtplei  12498  hashtpg  12499  strlemor3  14600  strle3  14604  lsptpcl  17496  perfectlem2  23374  constr2spthlem1  24465  ex-un  25014  ex-ss  25017  ex-pw  25019  sltsolem1  29400  bpoly3  29792  estrreslem2  32490  estrres  32491  dvh4dimlem  36893  dvhdimlem  36894  dvh4dimN  36897
  Copyright terms: Public domain W3C validator