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

Definition df-tp 3535
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 3529 . 2 class {𝐴, 𝐵, 𝐶}
51, 2cpr 3528 . . 3 class {𝐴, 𝐵}
63csn 3527 . . 3 class {𝐶}
75, 6cun 3069 . 2 class ({𝐴, 𝐵} ∪ {𝐶})
84, 7wceq 1331 1 wff {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
Colors of variables: wff set class
This definition is referenced by:  eltpg  3571  raltpg  3579  rextpg  3580  tpeq1  3612  tpeq2  3613  tpeq3  3614  tpcoma  3620  tpass  3622  qdass  3623  tpidm12  3625  diftpsn3  3664  snsstp1  3673  snsstp2  3674  snsstp3  3675  prsstp12  3676  tpss  3688  tpssi  3689  ord3ex  4117  tpexg  4368  dmtpop  5017  funtpg  5177  funtp  5179  fntpg  5182  ftpg  5607  fvtp1g  5631  tpfidisj  6819  fztp  9882  sumtp  11207  strle3g  12077  bdctp  13214
  Copyright terms: Public domain W3C validator