NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-tp GIF version

Definition df-tp 3743
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} ∪ {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 3739 . 2 class {A, B, C}
51, 2cpr 3738 . . 3 class {A, B}
63csn 3737 . . 3 class {C}
75, 6cun 3207 . 2 class ({A, B} ∪ {C})
84, 7wceq 1642 1 wff {A, B, C} = ({A, B} ∪ {C})
Colors of variables: wff setvar class
This definition is referenced by:  eltpg  3769  raltpg  3777  rextpg  3778  tpeq1  3808  tpeq2  3809  tpeq3  3810  tpcoma  3816  tpass  3818  qdass  3819  tpidm12  3821  diftpsn3  3849  snsstp1  3858  snsstp2  3859  snsstp3  3860  sstp  3870  tpss  3871  dmtpop  5071  2p1e3c  6156
  Copyright terms: Public domain W3C validator