Theorem nftru 1730

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1487	. 2 ⊢ ⊤
2	1	nfth 1727	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1484  Ⅎwnf 1708

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

This theorem depends on definitions:  df-bi 197  df-tru 1486  df-nf 1710

This theorem is referenced by:  nfeu  2486  nfmo  2487  nfceqi  2761  dvelimc  2787  nfral  2945  nfrex  3007  nfreu  3114  nfrmo  3115  nfrab  3123  rabtru  3361  nfsbc  3457  nfcsb  3551  nfdisj  4632  nfiota  5855  nfriota  6620  nfixp  7927  eqri  29315  esumnul  30110  hasheuni  30147  wl-cbvalnae  33320  wl-equsal  33326  limsup10ex  40005  liminf10ex  40006  liminfvalxr  40015  liminf0  40025  stowei  40281  ioosshoi  40883  vonioolem2  40895