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

Definition df-tp 3383
 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 3377 . 2 class {𝐴, 𝐵, 𝐶}
51, 2cpr 3376 . . 3 class {𝐴, 𝐵}
63csn 3375 . . 3 class {𝐶}
75, 6cun 2915 . 2 class ({𝐴, 𝐵} ∪ {𝐶})
84, 7wceq 1243 1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
 Colors of variables: wff set class This definition is referenced by:  eltpg  3416  raltpg  3423  rextpg  3424  tpeq1  3456  tpeq2  3457  tpeq3  3458  tpcoma  3464  tpass  3466  qdass  3467  tpidm12  3469  diftpsn3  3505  snsstp1  3514  snsstp2  3515  snsstp3  3516  prsstp12  3517  tpss  3529  tpssi  3530  ord3ex  3941  tpexg  4179  dmtpop  4796  funtpg  4950  funtp  4952  fntpg  4955  ftpg  5347  fvtp1g  5369  fztp  8940  bdctp  9992
 Copyright terms: Public domain W3C validator