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

Definition df-tp 4032
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 4031 . 2  class  { A ,  B ,  C }
51, 2cpr 4029 . . 3  class  { A ,  B }
63csn 4027 . . 3  class  { C }
75, 6cun 3474 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1379 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff setvar class
This definition is referenced by:  eltpg  4069  raltpg  4078  rextpg  4079  tpeq1  4115  tpeq2  4116  tpeq3  4117  tpcoma  4123  tpass  4125  qdass  4126  tpidm12  4128  diftpsn3  4165  tpprceq3  4167  tppreqb  4168  snsstp1  4178  snsstp2  4179  snsstp3  4180  sstp  4191  tpss  4192  tpssi  4193  ord3ex  4637  dmtpop  5482  funtpg  5636  funtp  5638  fntpg  5641  ftpg  6069  fvtp1  6106  fvtp1g  6109  tpex  6581  fr3nr  6593  tpfi  7792  fztp  11732  hashtplei  12484  hashtpg  12485  strlemor3  14580  strle3  14584  lsptpcl  17408  perfectlem2  23233  constr2spthlem1  24272  ex-un  24822  ex-ss  24825  ex-pw  24827  sltsolem1  29005  bpoly3  29397  dvh4dimlem  36240  dvhdimlem  36241  dvh4dimN  36244
  Copyright terms: Public domain W3C validator