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

Definition df-tp 3861
Description: Define unordered triple of classes. Definition of [Enderton] p. 19. (Contributed by NM, 9-Apr-1994.)
Assertion
Ref Expression
df-tp

Detailed syntax breakdown of Definition df-tp
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cC . . 3
41, 2, 3ctp 3855 . 2
51, 2cpr 3854 . . 3
63csn 3853 . . 3
75, 6cun 3303 . 2
84, 7wceq 1687 1
Colors of variables: wff setvar class
This definition is referenced by:  eltpg  3895  raltpg  3904  rextpg  3905  tpeq1  3938  tpeq2  3939  tpeq3  3940  tpcoma  3946  tpass  3948  qdass  3949  tpidm12  3951  diftpsn3  3987  tpprceq3  3988  tppreqb  3989  snsstp1  3999  snsstp2  4000  snsstp3  4001  sstp  4012  tpss  4013  tpssi  4014  ord3ex  4454  dmtpop  5287  funtpg  5438  funtp  5440  fntpg  5443  ftpg  5861  fvtp1  5894  fvtp1g  5897  tpex  6349  fr3nr  6361  tpfi  7546  fztp  11454  hashtplei  12126  hashtpg  12127  strlemor3  14207  strle3  14211  lsptpcl  16869  perfectlem2  22310  constr2spthlem1  23172  ex-un  23310  ex-ss  23313  ex-pw  23315  sltsolem1  27511  bpoly3  27903  dvh4dimlem  34525  dvhdimlem  34526  dvh4dimN  34529
  Copyright terms: Public domain W3C validator