Deductive databases extend traditional databases by integrating logic-based inference rules, offering capabilities beyond simple data retrieval and enabling complex queries and data derivations. These systems are especially valuable for applications that require inferring new relationships and insights from existing data using logical rules. Equality is a fundamental concept in computer science, with critical applications in areas like formal verification, compiler optimization, and theorem proving. Integrating equality into deductive databases significantly extends their utility, enabling efficient and robust equational reasoning for more sophisticated data analysis and transformations. In this paper, I introduce a proof system P≡ for deductive databases extended with equality. This system offers a formal mechanism for reasoning about equivalences within the context of logic-based inference rules commonly used in deductivedatabases.