Theorem nftru 1631

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

Assertion

Ref	Expression
nftru	|- F/ x T.

Proof of Theorem nftru

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

Syntax hints:   T. wtru 1399   F/wnf 1621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623

This theorem depends on definitions:  df-bi 185  df-tru 1401  df-nf 1622

This theorem is referenced by:  nfeu  2302  nfmo  2303  nfceqi  2612  dvelimc  2640  nfral  2840  nfrex  2917  nfreu  3029  nfrmo  3030  nfrab  3036  nfsbc  3346  nfcsb  3438  nfdisj  4422  nfiota  5538  nfriota  6241  nfixp  7481  rabtru  27601  eqri  27613  esumnul  28280  hasheuni  28317  wl-cbvalnae  30229  wl-equsal  30236  dvtanlem  30307  stowei  32088