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

Definition df-tp 3985
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 3984 . 2  class  { A ,  B ,  C }
51, 2cpr 3982 . . 3  class  { A ,  B }
63csn 3980 . . 3  class  { C }
75, 6cun 3414 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1455 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff setvar class
This definition is referenced by:  eltpg  4026  raltpg  4035  rextpg  4036  tpeq1  4073  tpeq2  4074  tpeq3  4075  tpcoma  4081  tpass  4083  qdass  4084  tpidm12  4086  diftpsn3  4123  tpprceq3  4125  tppreqb  4126  snsstp1  4136  snsstp2  4137  snsstp3  4138  sstp  4149  tpss  4150  tpssi  4151  ord3ex  4610  dmtpop  5335  funtpg  5655  funtp  5657  fntpg  5660  funcnvtp  5663  ftpg  6103  fvtp1  6140  fvtp1g  6143  tpex  6622  fr3nr  6638  tpfi  7878  fztp  11887  hashtplei  12679  hashtpg  12680  s3tpop  13046  sumtp  13865  bpoly3  14166  strlemor3  15274  strle3  15278  estrreslem2  16078  estrres  16079  lsptpcl  18257  perfectlem2  24214  constr2spthlem1  25380  ex-un  25930  ex-ss  25933  ex-pw  25935  sltsolem1  30607  dvh4dimlem  35057  dvhdimlem  35058  dvh4dimN  35061  perfectALTVlem2  38979
  Copyright terms: Public domain W3C validator