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

Definition df-tp 3849
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 3843 . 2
51, 2cpr 3842 . . 3
63csn 3841 . . 3
75, 6cun 3307 . 2
84, 7wceq 1654 1
Colors of variables: wff set class
This definition is referenced by:  eltpg  3879  raltpg  3887  rextpg  3888  tpeq1  3920  tpeq2  3921  tpeq3  3922  tpcoma  3928  tpass  3930  qdass  3931  tpidm12  3933  diftpsn3  3965  tpprceq3  3966  tppreqb  3967  snsstp1  3977  snsstp2  3978  snsstp3  3979  sstp  3991  tpss  3992  tpssi  3993  ord3ex  4428  tpex  4749  fr3nr  4801  dmtpop  5392  funtpg  5548  funtp  5550  fntpg  5553  ftpg  5964  fvtp1  5987  fvtp1g  5990  tpfi  7431  fztp  11153  hashtplei  11741  hashtpg  11742  strlemor3  13609  strle3  13613  lsptpcl  16106  perfectlem2  21065  constr2spthlem1  21645  ex-un  21783  ex-ss  21786  ex-pw  21788  sltsolem1  25727  bpoly3  26208  dvh4dimlem  32481  dvhdimlem  32482  dvh4dimN  32485
  Copyright terms: Public domain W3C validator