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

Definition df-tp 3724
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 3718 . 2  class  { A ,  B ,  C }
51, 2cpr 3717 . . 3  class  { A ,  B }
63csn 3716 . . 3  class  { C }
75, 6cun 3226 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1642 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff set class
This definition is referenced by:  eltpg  3752  raltpg  3760  rextpg  3761  tpeq1  3791  tpeq2  3792  tpeq3  3793  tpcoma  3799  tpass  3801  qdass  3802  tpidm12  3804  diftpsn3  3835  snsstp1  3845  snsstp2  3846  snsstp3  3847  sstp  3859  tpss  3860  ord3ex  4281  tpex  4601  fr3nr  4653  dmtpop  5231  funtp  5385  fvtp1  5808  tpfi  7222  fztp  10933  hashtplei  11476  strlemor3  13334  strle3  13338  lsptpcl  15835  perfectlem2  20581  ex-un  20923  ex-ss  20926  ex-pw  20928  sltsolem1  24880  bpoly3  25352  ftp  26216  tpprceq3  27407  tppreqb  27408  funtpg  27415  fntpg  27416  ftpg  27417  fvtp1g  27420  hashtpg  27471  constr2trl  27734  dvh4dimlem  31702  dvhdimlem  31703  dvh4dimN  31706
  Copyright terms: Public domain W3C validator