Metamath Proof Explorer

Theorem nftru

Description: 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)

Ref Expression
Assertion nftru
|- F/ x T.


Step Hyp Ref Expression
1 tru
 |-  T.
2 1 nfth
 |-  F/ x T.