Axiom ax_8 | index | src |

Elementhood respects equality. This is a theorem for most definitions but has to be axiomatized for primitive term constructors like e. This is Axiom 8 of predicate logic (which has an instance for every primitive predicate in the language).

axiom ax_8 (a b: nat) (A: set): $ a = b -> a e. A -> b e. A $;