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

Definition df-tp 3737
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 3731 . 2  class  { A ,  B ,  C }
51, 2cpr 3730 . . 3  class  { A ,  B }
63csn 3729 . . 3  class  { C }
75, 6cun 3236 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1647 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff set class
This definition is referenced by:  eltpg  3766  raltpg  3774  rextpg  3775  tpeq1  3807  tpeq2  3808  tpeq3  3809  tpcoma  3815  tpass  3817  qdass  3818  tpidm12  3820  diftpsn3  3852  tpprceq3  3853  tppreqb  3854  snsstp1  3864  snsstp2  3865  snsstp3  3866  sstp  3878  tpss  3879  ord3ex  4302  tpex  4622  fr3nr  4674  dmtpop  5252  funtpg  5405  funtp  5407  fntpg  5410  ftpg  5817  fvtp1  5839  fvtp1g  5842  tpfi  7279  fztp  10994  hashtplei  11577  hashtpg  11578  strlemor3  13445  strle3  13449  lsptpcl  15946  perfectlem2  20692  ex-un  21122  ex-ss  21125  ex-pw  21127  sltsolem1  25063  bpoly3  25535  ftp  26399  constr2trl  27736  dvh4dimlem  31704  dvhdimlem  31705  dvh4dimN  31708
  Copyright terms: Public domain W3C validator