Axiom elab | index | src |

a is in {x | p(x)} iff p(a) holds.

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