Theorem nftru 1801

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1537	. 2 ⊢ ⊤
2	1	nfth 1798	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1534  Ⅎwnf 1780

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

This theorem depends on definitions:  df-bi 209  df-tru 1536  df-nf 1781

This theorem is referenced by:  nfsb  2561  nfmov  2640  nfmo  2642  nfeuw  2675  nfeu  2676  nfceqiOLD  2974  dvelimc  3006  nfralw  3225  nfral  3226  nfrex  3309  nfrexg  3310  nfreuw  3374  nfrmow  3375  nfreu  3376  nfrmo  3377  nfrabw  3385  nfrab  3386  rabtru  3676  nfsbcw  3793  nfsbc  3796  nfcsbw  3908  nfcsb  3909  eqri  3986  nfdisjw  5035  nfdisj  5036  nfiotaw  6312  nfiota  6314  nfriota  7120  nfixpw  8474  nfixp  8475  esumnul  31302  hasheuni  31339  wl-cbvalnae  34767  wl-equsal  34774  limsup10ex  42047  liminf10ex  42048  liminfvalxr  42057  liminf0  42067  stowei  42343  ioosshoi  42945  vonioolem2  42957