Higher-Order Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HOLE Home  >  Th. List  >  ax-tdef Unicode version

Axiom ax-tdef 164
 Description: The type definition axiom. The last hypothesis corresponds to the actual definition one wants to make; here we are defining a new type and the definition will provide us with pair of bijections mapping the new type to the subset of the old type such that is true. In order for this to be a valid (conservative) extension, we must ensure that the new type is non-empty, and for that purpose we need a witness that is not always false.
Hypotheses
Ref Expression
ax-tdef.1
ax-tdef.2
ax-tdef.3
ax-tdef.4 typedef
Assertion
Ref Expression
ax-tdef
Distinct variable groups:   ,   ,   ,

Detailed syntax breakdown of Axiom ax-tdef
StepHypRef Expression
1 kt 8 . 2 term
2 tal 112 . . . 4 term
3 hbe . . . . 5 type
4 vx . . . . 5 var
5 ta . . . . . . 7 term
6 tr . . . . . . . 8 term
73, 4tv 1 . . . . . . . 8 term
86, 7kc 5 . . . . . . 7 term
95, 8kc 5 . . . . . 6 term
10 ke 7 . . . . . 6 term
119, 7, 10kbr 9 . . . . 5 term
123, 4, 11kl 6 . . . 4 term
132, 12kc 5 . . 3 term
14 hal . . . . 5 type
15 tf . . . . . . 7 term
1614, 4tv 1 . . . . . . 7 term
1715, 16kc 5 . . . . . 6 term
185, 16kc 5 . . . . . . . 8 term
196, 18kc 5 . . . . . . 7 term
2019, 16, 10kbr 9 . . . . . 6 term
2117, 20, 10kbr 9 . . . . 5 term
2214, 4, 21kl 6 . . . 4 term
232, 22kc 5 . . 3 term
2413, 23kct 10 . 2 term
251, 24wffMMJ2 11 1 wff
 Colors of variables: type var term This axiom is referenced by: (None)
 Copyright terms: Public domain W3C validator