# Set membership

This English edition is an AI candidate and does not yet have an OCME Atlas (GPT-6) Twin closure receipt.

The notation x∈A states that the element x belongs to the set A.

mko-set-membership · definition · v0.8.0



## Mathematical statement

Given a set A and an object x, x∈A is a proposition stating that x is an element of A.





## Representative formula (exact TeX)

x\in A





## Assumptions


- A has been specified as a set.





## Symbol scope


- x — candidate element
- A — set
- ∈ — membership relation





## Intuition, definition, and misconceptions

A set can be understood as a mathematical whole made up of selected objects, without requiring a physical box or spatial container.

The expression x∈A states only a membership relation. It does not say that x equals A, and it does not say that x is a subset of A.

In the current Lean mapping, Set α is represented as α→Prop, so x∈A and A x are definitionally equivalent.

A common mistake is to confuse element membership x∈A with the subset relation B⊆A, or to treat programming-container membership as the semantics of every mathematical set theory.





## Adopted derivation guide

[Set membership: x∈A is a proposition, kept apart from ⊆, = and a program's membership test](https://ocme.evemisslab.com/en/derivations/derivation-mko-set-membership-01/)The original MKO is retained. The guide has its own append-only revision and verification boundaries, not a new Lean proof.





## Prerequisites







## Verification boundary

Lean formalizes membership when Set α is represented as α→Prop. This result does not claim to cover every foundation of set theory, and it does not automatically turn a programming container into a mathematical set.

formalized_lean_set_semantics


- [evidence-sha256-702de77019f352eb431eb67bd7b266491b7c36c922d952e44be2b11ba95bcb5d](https://ocme.evemisslab.com/data/evidence/702de77019f352eb431eb67bd7b266491b7c36c922d952e44be2b11ba95bcb5d.json)





## Next obligation

Extend the subset, set equality, and basic set-operation objects while keeping membership, inclusion, and equality as distinct relations.





## Same-source structured data

This page and the interactive view use the same object and existing language edition; this adds no proof or human review.

[Canonical MKO JSON](https://ocme.evemisslab.com/data/mko/set-membership.json) · [Plain Markdown](https://ocme.evemisslab.com/en/mko/mko-set-membership/index.md)