∈ \(\in\) — Primitive Class Membership Predicate (∈, AST Constructor: TpIn)
Undefinable primitive binary membership predicate x ∈ Y asserting that class x is an element of class Y (which implies x set by Entry DefIsSet (3.02)). Never used for typing (use :).
| Field | Mathematical & Kernel Specification (MKTD1 / MKTD2) |
|---|---|
| Symbol |
∈
\(\in\)
|
| Category | Predicate Symbol (Binary Primitive Relation) |
| SML AST Constructor | HP (TpIn of ('Class_EXP * 'Class_EXP)) [in datatype Truth_p, typetheory.ML:659] |
| Constructor Arguments | 1. Element class term x : Class; 2. Container class term Y : Class |
| Metatype / Signature | Class × Class → Bool | Class.Expression × Class.Expression → Fm |
| Binder Status | No — Primitive Binary Predicate Symbol (Undefinable Set/Class Membership) |
| Defining Kernel Entries (ML Labels) | Inference Rule RulClassComprehension (3.01): Class comprehension (#RulClassComprehension / #label-class-comprehension) |
| LaTeX Form | \in |
| How to Understand It | SML AST Constructor: |
| Canonical Law / Usage | ∀(X:Class)((X set) ⟷ (∃(Y:Class)(X ∈ Y))) |
| Related Symbols & Kernel Entries |
Defining Axioms, Rules & Formal Definitions (Rendered Directly from Kernel Entries)
Generated without code duplication by invoking render_entry_row_base "../manual.html" on the corresponding kernel Entry records.
| # | Formal Entity Specification | ||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 3.01 |
|