The true constant has no free variables. (This can also be proven in one step with nfv, but this proof does not use [ax-5] .) (Contributed by Mario Carneiro, 6-Oct-2016.)