Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-tp Structured version   GIF version

Definition df-tp 3375
 Description: Define unordered triple of classes. Definition of [Enderton] p. 19. (Contributed by NM, 9-Apr-1994.)
Assertion
Ref Expression
df-tp {A, B, 𝐶} = ({A, B} ∪ {𝐶})

Detailed syntax breakdown of Definition df-tp
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
3 cC . . 3 class 𝐶
41, 2, 3ctp 3369 . 2 class {A, B, 𝐶}
51, 2cpr 3368 . . 3 class {A, B}
63csn 3367 . . 3 class {𝐶}
75, 6cun 2909 . 2 class ({A, B} ∪ {𝐶})
84, 7wceq 1242 1 wff {A, B, 𝐶} = ({A, B} ∪ {𝐶})
 Colors of variables: wff set class This definition is referenced by:  eltpg  3407  raltpg  3414  rextpg  3415  tpeq1  3447  tpeq2  3448  tpeq3  3449  tpcoma  3455  tpass  3457  qdass  3458  tpidm12  3460  diftpsn3  3496  snsstp1  3505  snsstp2  3506  snsstp3  3507  prsstp12  3508  tpss  3520  tpssi  3521  ord3ex  3932  tpexg  4145  dmtpop  4739  funtpg  4893  funtp  4895  fntpg  4898  ftpg  5290  fvtp1g  5312  fztp  8690  bdctp  9307
 Copyright terms: Public domain W3C validator