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

Definition df-tp 3552
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 3546 . 2  class  { A ,  B ,  C }
51, 2cpr 3545 . . 3  class  { A ,  B }
63csn 3544 . . 3  class  { C }
75, 6cun 3076 . 2  class  ( { A ,  B }  u.  { C } )
84, 7wceq 1619 1  wff  { A ,  B ,  C }  =  ( { A ,  B }  u.  { C } )
Colors of variables: wff set class
This definition is referenced by:  eltpg  3580  raltpg  3588  rextpg  3589  tpeq1  3619  tpeq2  3620  tpeq3  3621  tpcoma  3627  tpass  3629  qdass  3630  tpidm12  3632  snsstp1  3666  snsstp2  3667  snsstp3  3668  sstp  3678  tpss  3679  ord3ex  4094  tpex  4410  fr3nr  4462  dmtpop  5055  funtp  5160  fvtp1  5576  tpfi  7017  fztp  10719  hashtplei  11257  strlemor3  13111  strle3  13115  lsptpcl  15571  perfectlem2  20301  ex-un  20624  ex-ss  20627  ex-pw  20629  axsltsolem1  23489  bpoly3  23967  ftp  26059  dvh4dimlem  30322  dvhdimlem  30323  dvh4dimN  30326
  Copyright terms: Public domain W3C validator