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

Definition df-tp 3411
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 class 𝐴
2 cB . . 3 class 𝐵
3 cC . . 3 class 𝐶
41, 2, 3ctp 3405 . 2 class {𝐴, 𝐵, 𝐶}
51, 2cpr 3404 . . 3 class {𝐴, 𝐵}
63csn 3403 . . 3 class {𝐶}
75, 6cun 2943 . 2 class ({𝐴, 𝐵} ∪ {𝐶})
84, 7wceq 1259 1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
Colors of variables: wff set class
This definition is referenced by:  eltpg  3444  raltpg  3451  rextpg  3452  tpeq1  3484  tpeq2  3485  tpeq3  3486  tpcoma  3492  tpass  3494  qdass  3495  tpidm12  3497  diftpsn3  3533  snsstp1  3542  snsstp2  3543  snsstp3  3544  prsstp12  3545  tpss  3557  tpssi  3558  ord3ex  3969  tpexg  4207  dmtpop  4824  funtpg  4978  funtp  4980  fntpg  4983  ftpg  5375  fvtp1g  5397  fztp  9042  bdctp  10379
  Copyright terms: Public domain W3C validator