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

Definition df-tp 3439
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 3433 . 2 class {𝐴, 𝐵, 𝐶}
51, 2cpr 3432 . . 3 class {𝐴, 𝐵}
63csn 3431 . . 3 class {𝐶}
75, 6cun 2986 . 2 class ({𝐴, 𝐵} ∪ {𝐶})
84, 7wceq 1287 1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
Colors of variables: wff set class
This definition is referenced by:  eltpg  3473  raltpg  3480  rextpg  3481  tpeq1  3513  tpeq2  3514  tpeq3  3515  tpcoma  3521  tpass  3523  qdass  3524  tpidm12  3526  diftpsn3  3563  snsstp1  3572  snsstp2  3573  snsstp3  3574  prsstp12  3575  tpss  3587  tpssi  3588  ord3ex  4001  tpexg  4245  dmtpop  4874  funtpg  5032  funtp  5034  fntpg  5037  ftpg  5446  fvtp1g  5468  tpfidisj  6592  fztp  9425  sumtp  10695  bdctp  11232
  Copyright terms: Public domain W3C validator