equ-ax
Top-level context. Axioms for equality and substitution.
Description:
Axioms 8, 9, 11, and the definition of proper
substitution are stated for set terms (st) to be introduced with the
iota descriptor. Our axioms 9 and 11 also have distinct variable
conditions.
Primitive symbols:
Axioms:
| Name | Comment |
| ax10 | Axiom of Quantifier Substitution |
| ax11 | Axiom of Variable Substitution |
| ax12 | Axiom of Quantifier Introduction |
| ax16 | Axiom of Distinct Variables (1) |
| ax17 | Axiom of Distinct Variables (2) |
| ax8 | Axiom of Equality |
| ax9 | Axiom of Existence |
Definitions:
| Name | Sym | Comment |
| df-sb | [ / ] | Proper Substitution. |
)