Underlying Axioms

• 692: 1.1: Straight Line Determined by Two Distinct Points
• 694: 1.2: Circle Determined by its Center and its Radius
• 734: 1.3: Segment Extension
• 682: Axiom of Distributivity
• 666: Axiom of Empty Set
• 551: Axiom of Extensionality
• 717: Axiom of Foundation
• 678: Axiom of Infinity
• 716: Axiom of Power Set
• 675: Axiom of Separation (Restricted Principle of Comprehension)
• 705: Bivalence of Truth
• 504: Peano Axioms
• 1427: Zermelo-Fraenkel Axioms

Logical Predecessors

• Definitions:
  • 572: Reflexive, Symmetric and Transitive Binary Relations
  • 571: Relation
  • 550: Set, Set Element, Empty Set

Logical Successors

• Definitions:
  • 6330: Canonical Projection
  • 7992: Complete System of Representatives
  • 7990: Equivalence Class
  • 7989: Inverse Relation
• Theorems:
  • 980: Cardinal Number
  • 8154: Congruence Classes
  • 1221: Connectivity Is an Equivalence Relation - Components Are a Partition of a Graph
  • 888: Construction of Fields from Integral Domains
  • 839: Construction of Groups from Commutative and Cancellative Semigroups
  • 982: Counting the Set's Elements Using Its Partition
  • 844: Definition of Integers
  • 1033: Definition of Rational Numbers
  • 1105: Definition of Real Numbers
  • 6328: Equivalency of Vectors in Vector Space If their Difference Forms a Subspace
  • 6360: Equivalent Knot Diagrams
  • 8009: Functions Constitute Equivalence Relations
  • 829: Properties of Cosets
  • 71: Quotient Space
  • 6196: Sum of Euler Function
  • 1539: The Equality of Sets Is an Equivalence Relation