Alphabeta MathHow 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 Axiom of Extensionality:
Definition
The Axiom of Extensionality is the sentence
of the language of set theory (The first-order language of set theory: , , formulas with parameters, and class abbreviations): if every satisfies if and only if , then .
A set is therefore determined by its members and by nothing else. Order, repetition and any description used to present a set are invisible to identity.
Remarks
-
The converse is logic, not an axiom. If then and are the same statement for every , by the substitution rule for equality. So Extensionality upgrades to the biconditional , and only the right-to-left direction of that biconditional — the implication from sameness of members to equality — is assumed.
-
What it is used for below. Every construction on this page produces a set by an axiom that specifies its members, and every such axiom is stated with . Extensionality is what turns "a set with these members" into "the set with these members", so it is the licence for each definite article and each piece of notation introduced here.
Depends on
Used by
- For a nonempty index set I: B ∩ ⋃_i ∈ I Aᵢ = ⋃_i ∈ I (B ∩ Aᵢ), B ∪ ⋂_i ∈ I Aᵢ = ⋂_i ∈ I (B ∪ Aᵢ), X ∖ ⋃_i ∈ I Aᵢ = ⋂_i ∈ I (X ∖ Aᵢ), and X ∖ ⋂_i ∈ I Aᵢ = ⋃_i ∈ I (X ∖ Aᵢ) Corollary
- For f : A → B: S ⊆ f⁻¹[f[S]] for every S ⊆ A, with equality for every such S if and only if f is injective; and f[f⁻¹[T]] = T ∩ f[A] for every T ⊆ B, so equality with T holds for every such T if and only if f is surjective Corollary
- Relations R and S on a two-element set with S ∘ R ≠ R ∘ S Counterexample
- Sets A, B, C with (A × B) × C ≠ A × (B × C) Counterexample
- Subset x ⊆ y, proper subset x ⊊ y, and the separation notation { z ∈ x : φ(z) } Definition
- The difference a ∖ b, the symmetric difference a △ b, and the complement X ∖ a relative to a set X Definition
- The set of first-order ZF axiom sentences Definition
- The union ⋃ x of a set, and the binary union a ∪ b := ⋃ {a,b} Definition
- The unordered pair {x,y} and the singleton {x} = {x,x} Definition
- (∅,∅) = {{∅}} and (∅,{∅}) = {{∅},{∅,{∅}}}, with the characterising property checked on them Example
- {∅} × {∅,{∅}} listed in full, together with the inclusion in P(P(A ∪ B)) that makes it a set Example
- ⋃ ⋂ (a,b) = a for all a and b, and ⋃(a,b) = {a,b}, so both coordinates are recovered from the pair as a set Example
- A four-pair relation on {∅,{∅},{∅,{∅}}} with its domain, range, field, inverse, restriction, image and self-composite computed Example
- A two-cell partition of a three-element set, the equivalence relation it induces listed pair by pair, and the quotient set recovered from it Example
- P(∅) = {∅}, P({∅}) = {∅,{∅}}, and P({∅,{∅}}) listed in full Example
- FALSE: (a ∖ b) ∖ c = a ∖ (b ∖ c) for all sets a, b, c False statement
- {a,b} = {c,d} if and only if (a = c and b = d) or (a = d and b = c); in particular {a} = {c,d} if and only if a = c = d Lemma
- ∅ ⊆ x, x ⊆ x, inclusion is transitive, and x = y if and only if x ⊆ y and y ⊆ x Lemma
- ⋃ ∅ = ∅, ⋃ {a} = a, ⋃ {a,b} = a ∪ b, ⋂ {a} = a, and ⋂ {a,b} = a ∩ b Lemma
- For a set x ≠ ∅ the collection { z : ∀ s (s ∈ x → z ∈ s) } is a set, and it does not depend on the member of x used to separate it Lemma
- For every set x there is exactly one set whose elements are precisely the subsets of x Lemma
- Functions f and g are equal if and only if dom f = dom g and f(x) = g(x) for every x in that common domain Lemma
- The natural numbers exist: a smallest inductive set Lemma
- ∏_i ∈ ∅ Aᵢ = {∅}; if Aⱼ = ∅ for some j ∈ I then ∏_i ∈ I Aᵢ = ∅; and for I = {j} the evaluation f ↦ f(j) is a bijection ∏_i ∈ I Aᵢ → Aⱼ Proposition
- A × (B ∪ C) = (A × B) ∪ (A × C), A × (B ∩ C) = (A × B) ∩ (A × C), A × (B ∖ C) = (A × B) ∖ (A × C), (A ∩ B) × (C ∩ D) = (A × C) ∩ (B × D); A × B = ∅ if and only if A = ∅ or B = ∅; and for nonempty A and B, A × B ⊆ C × D if and only if A ⊆ C and B ⊆ D Proposition
- For f : A → B and S, T ⊆ A: f[S ∪ T] = f[S] ∪ f[T], f[S ∩ T] ⊆ f[S] ∩ f[T] and f[S] ∖ f[T] ⊆ f[S ∖ T]; both inclusions are equalities for all S and T if and only if f is injective Proposition
- P(∅) = {∅}; ∅ ∈ P(a) and a ∈ P(a); a ⊆ b if and only if P(a) ⊆ P(b); ⋃ P(a) = a; ⋂ P(a) = ∅; and P(a ∩ b) = P(a) ∩ P(b) while only P(a) ∪ P(b) ⊆ P(a ∪ b) holds Proposition
- R[A ∪ B] = R[A] ∪ R[B], R[A ∩ B] ⊆ R[A] ∩ R[B], R[A] ∖ R[B] ⊆ R[A ∖ B], A ⊆ B implies R[A] ⊆ R[B], and (S ∘ R)[A] = S[R[A]] Proposition
- T ∘ (S ∘ R) = (T ∘ S) ∘ R, (S ∘ R)⁻¹ = R⁻¹ ∘ S⁻¹, (R⁻¹)⁻¹ = R, dom(R⁻¹) = ran R, and Δ_B ∘ R = R = R ∘ Δ_A for a relation R from A to B Proposition
- Union and intersection are commutative, associative, idempotent and absorptive; a ∪ ∅ = a, a ∩ ∅ = ∅, a ∖ ∅ = a, a ∖ a = ∅; and a ⊆ b if and only if a ∪ b = b, if and only if a ∩ b = a, if and only if a ∖ b = ∅ Proposition
- The axiom ledger for this page: which of the ZFC axioms each construction and each result actually consumes Remark
- a ∩ (b ∪ c) = (a ∩ b) ∪ (a ∩ c) and a ∪ (b ∩ c) = (a ∪ b) ∩ (a ∪ c); and for a nonempty set F, a ∩ ⋃ F = ⋃ { a ∩ b : b ∈ F } and a ∪ ⋂ F = ⋂ { a ∪ b : b ∈ F } Theorem
- For f : A → B and T, U ⊆ B: f⁻¹[T ∪ U] = f⁻¹[T] ∪ f⁻¹[U], f⁻¹[T ∩ U] = f⁻¹[T] ∩ f⁻¹[U], f⁻¹[T ∖ U] = f⁻¹[T] ∖ f⁻¹[U], and f⁻¹[B ∖ T] = A ∖ f⁻¹[T] Theorem
- On a set A, R ↦ R ∖ Δ_A and S ↦ S ∪ Δ_A are mutually inverse bijections between the partial orders on A and the irreflexive, transitive relations on A; R ∖ Δ_A is the strict order of R, and every irreflexive transitive relation is asymmetric Theorem
- There is exactly one set with no elements, written ∅ Theorem
- X ∖ (a ∪ b) = (X ∖ a) ∩ (X ∖ b) and X ∖ (a ∩ b) = (X ∖ a) ∪ (X ∖ b); and for a nonempty set F, X ∖ ⋃ F = ⋂ { X ∖ a : a ∈ F } and X ∖ ⋂ F = ⋃ { X ∖ a : a ∈ F } Theorem
Dependency tree · one level
1 result within one dependency step of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- B. Kaya, MATH 320 Set Theory (METU), Axiom 2 (standard reference, not scraped)
- Axiom of extensionality (Wikipedia) (standard reference, not scraped)
- Zermelo-Fraenkel set theory (Wikipedia) (standard reference, not scraped)