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

Definition df-ot 3356
Description: Define ordered triple of classes. Definition of ordered triple in [Stoll] p. 25. (Contributed by NM, 3-Apr-2015.)
Assertion
Ref Expression
df-ot A, B, 𝐶⟩ = ⟨⟨A, B⟩, 𝐶

Detailed syntax breakdown of Definition df-ot
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
3 cC . . 3 class 𝐶
41, 2, 3cotp 3350 . 2 class A, B, 𝐶
51, 2cop 3349 . . 3 class A, B
65, 3cop 3349 . 2 class ⟨⟨A, B⟩, 𝐶
74, 6wceq 1226 1 wff A, B, 𝐶⟩ = ⟨⟨A, B⟩, 𝐶
Colors of variables: wff set class
This definition is referenced by:  oteq1  3528  oteq2  3529  oteq3  3530  otexg  3937  otth  3949  fnotovb  5467  ot1stg  5698  ot2ndg  5699  ot3rdgg  5700  ottposg  5788
  Copyright terms: Public domain W3C validator