DefinitionDefinition: Literature-sourcedProof: Not applicableverified 2026-08-06 (claude-opus-5)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The power set $P (x) = {z : z \subseteq x}$

Let $x$ be a set. By For every set $x$ there is exactly one set whose elements are precisely the subsets of $x$ there is exactly one set whose elements are precisely the subsets of $x$ (Subset $x \subseteq y$ , proper subset $x ⊊ y$ , and the separation notation ${z \in x : φ (z)}$ ); it is the power set of $x$ , written $P (x)$ . Thus $z \in P (x)$ holds if and only if $z \subseteq x$ , and in the class notation of the page,

$P (x) = {z : z \subseteq x} .$

Two axioms, not one. The elements of $P (x)$ are pinned down by The Axiom of Power Set: $\forall x \exists y \forall z (\forall t (t \in z \to t \in x) \to z \in y)$ together with The Axiom Schema of Separation: for each formula $φ$ , $\forall \overset{ˉ}{p} \forall x \exists y \forall z (z \in y \leftrightarrow (z \in x \land φ (z, \overset{ˉ}{p})))$ , because the axiom is assumed here only in its implication form. The axiom ledger for this page: which of the ZFC axioms each construction and each result actually consumes keeps that cost visible.
The power set is never empty. $\emptyset \subseteq x$ always holds, so $\emptyset \in P (x)$ for every $x$ ; in particular $P (\emptyset) = {\emptyset}$ rather than $\emptyset$ . That and the other basic identities are $P (\emptyset) = {\emptyset}$ ; $\emptyset \in P (a)$ and $a \in P (a)$ ; $a \subseteq b$ if and only if $P (a) \subseteq P (b)$ ; $⋃ P (a) = a$ ; $⋂ P (a) = \emptyset$ ; and $P (a \cap b) = P (a) \cap P (b)$ while only $P (a) \cup P (b) \subseteq P (a \cup b)$ holds.

Depends on