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

Definition df-tp 3902
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 3896 . 2
51, 2cpr 3895 . . 3
63csn 3894 . . 3
75, 6cun 3351 . 2
84, 7wceq 1662 1
Colors of variables: wff set class
This definition is referenced by:  eltpg  3935  raltpg  3944  rextpg  3945  tpeq1  3977  tpeq2  3978  tpeq3  3979  tpcoma  3985  tpass  3987  qdass  3988  tpidm12  3990  diftpsn3  4022  tpprceq3  4023  tppreqb  4024  snsstp1  4034  snsstp2  4035  snsstp3  4036  sstp  4048  tpss  4049  tpssi  4050  ord3ex  4489  dmtpop  5314  funtpg  5465  funtp  5467  fntpg  5470  ftpg  5878  fvtp1  5904  fvtp1g  5907  tpex  6345  fr3nr  6356  tpfi  7494  fztp  11308  hashtplei  11973  hashtpg  11974  strlemor3  14049  strle3  14053  lsptpcl  16558  perfectlem2  21523  constr2spthlem1  22103  ex-un  22241  ex-ss  22244  ex-pw  22246  sltsolem1  26453  bpoly3  26934  dvh4dimlem  33514  dvhdimlem  33515  dvh4dimN  33518
  Copyright terms: Public domain W3C validator