theorem nfab1 {x: nat} (p: wff x): $ FS/ x {x | p} $;
y e. {x | p} <-> [y / x] p
F/ x [y / x] p
F/ x y e. {x | p}
FS/ x {x | p}