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

Definition df-tp 3917
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 3911 . 2
51, 2cpr 3910 . . 3
63csn 3909 . . 3
75, 6cun 3363 . 2
84, 7wceq 1670 1
Colors of variables: wff set class
This definition is referenced by:  eltpg  3950  raltpg  3959  rextpg  3960  tpeq1  3992  tpeq2  3993  tpeq3  3994  tpcoma  4000  tpass  4002  qdass  4003  tpidm12  4005  diftpsn3  4037  tpprceq3  4038  tppreqb  4039  snsstp1  4049  snsstp2  4050  snsstp3  4051  sstp  4063  tpss  4064  tpssi  4065  ord3ex  4505  dmtpop  5335  funtpg  5486  funtp  5488  fntpg  5491  ftpg  5907  fvtp1  5940  fvtp1g  5943  tpex  6389  fr3nr  6401  tpfi  7548  fztp  11365  hashtplei  12033  hashtpg  12034  strlemor3  14112  strle3  14116  lsptpcl  16674  perfectlem2  22035  constr2spthlem1  22615  ex-un  22753  ex-ss  22756  ex-pw  22758  sltsolem1  26962  bpoly3  27443  dvh4dimlem  33791  dvhdimlem  33792  dvh4dimN  33795
  Copyright terms: Public domain W3C validator