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

Definition df-tp 3615
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 3609 . 2 class {𝐴, 𝐵, 𝐶}
51, 2cpr 3608 . . 3 class {𝐴, 𝐵}
63csn 3607 . . 3 class {𝐶}
75, 6cun 3142 . 2 class ({𝐴, 𝐵} ∪ {𝐶})
84, 7wceq 1364 1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
Colors of variables: wff set class
This definition is referenced by:  eltpg  3652  raltpg  3660  rextpg  3661  tpeq1  3693  tpeq2  3694  tpeq3  3695  tpcoma  3701  tpass  3703  qdass  3704  tpidm12  3706  diftpsn3  3748  snsstp1  3757  snsstp2  3758  snsstp3  3759  prsstp12  3760  tpss  3773  tpssi  3774  ord3ex  4208  tpexg  4462  dmtpop  5122  funtpg  5286  funtp  5288  fntpg  5291  ftpg  5721  fvtp1g  5745  tpfidisj  6957  fztp  10110  sumtp  11457  strle3g  12623  lsptpcl  13727  bdctp  15102
  Copyright terms: Public domain W3C validator