ATLAS Ouvrir dans l'atlas →

AxiomeAxiomes de ZF

Axiome des parties

On note 𝒫(A){\mathcal P}(A) cet ensemble, unique par extensionnalité.

Énoncé
∀A ∃P ∀x [x∈P⇔x⊂A].\forall A\, \exists P\, \forall x\, \big[x \in P \Leftrightarrow x \subset A\big].
Remarque

Il permet de former le produit cartésien, défini au nœud Produit cartésien, par séparation dans 𝒫(𝒫(A∪B))\mathcal P(\mathcal P(A \cup B)) ; le schéma de remplacement en donnerait une autre construction, sans lui.

Ouvrir dans l'atlas interactif →