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  4391  tpex  4710  fr3nr  4762  dmtpop  5348  funtpg  5503  funtp  5505  fntpg  5508  ftpg  5918  fvtp1  5941  fvtp1g  5944  tpfi  7384  fztp  11104  hashtplei  11692  hashtpg  11693  strlemor3  13560  strle3  13564  lsptpcl  16057  perfectlem2  21016  constr2spthlem1  21596  ex-un  21734  ex-ss  21737  ex-pw  21739  sltsolem1  25625  bpoly3  26106  dvh4dimlem  32303  dvhdimlem  32304  dvh4dimN  32307
  Copyright terms: Public domain W3C validator