Theorem nftru 1677

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

Assertion

Ref	Expression
nftru	|- F/ x T.

Proof of Theorem nftru

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

Syntax hints:   T. wtru 1445   F/wnf 1667

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

This theorem depends on definitions:  df-bi 189  df-tru 1447  df-nf 1668

This theorem is referenced by:  nfeu  2315  nfmo  2316  nfceqi  2589  dvelimc  2614  nfral  2774  nfrex  2850  nfreu  2965  nfrmo  2966  nfrab  2972  nfsbc  3289  nfcsb  3381  nfdisj  4385  nfiota  5550  nfriota  6261  nfixp  7541  rabtru  28135  eqri  28147  esumnul  28869  hasheuni  28906  wl-cbvalnae  31866  wl-equsal  31873  dvtanlemOLD  31991  stowei  37926