a is in {x | p(x)} iff p(a) holds.
a
{x | p(x)}
p(a)
axiom elab (a: nat) {x: nat} (p: wff x): $ a e. {x | p} <-> [a / x] p $;