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 $;