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

Definition df-tp 3824
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 3818 . 2  class  { A ,  B ,  C }
51, 2cpr 3817 . . 3  class  { A ,  B }
63csn 3816 . . 3  class  { C }
75, 6cun 3320 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1653 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff set class
This definition is referenced by:  eltpg  3853  raltpg  3861  rextpg  3862  tpeq1  3894  tpeq2  3895  tpeq3  3896  tpcoma  3902  tpass  3904  qdass  3905  tpidm12  3907  diftpsn3  3939  tpprceq3  3940  tppreqb  3941  snsstp1  3951  snsstp2  3952  snsstp3  3953  sstp  3965  tpss  3966  tpssi  3967  ord3ex  4392  tpex  4711  fr3nr  4763  dmtpop  5349  funtpg  5504  funtp  5506  fntpg  5509  ftpg  5919  fvtp1  5942  fvtp1g  5945  tpfi  7385  fztp  11107  hashtplei  11695  hashtpg  11696  strlemor3  13563  strle3  13567  lsptpcl  16060  perfectlem2  21019  constr2spthlem1  21599  ex-un  21737  ex-ss  21740  ex-pw  21742  sltsolem1  25628  bpoly3  26109  dvh4dimlem  32315  dvhdimlem  32316  dvh4dimN  32319
  Copyright terms: Public domain W3C validator