Theorem nftru 1806

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1546	. 2 ⊢ ⊤
2	1	nfth 1803	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 207  df-tru 1545  df-nf 1786

This theorem is referenced by:  nfsb  2527  nfmov  2560  nfmo  2562  nfeuw  2593  nfeu  2594  dvelimc  2924  nfrexw  3285  nfral  3336  nfrex  3337  nfrmo  3387  nfreu  3388  nfrab  3427  rabtru  3632  nfsbcw  3750  nfsbc  3753  nfcsbw  3863  nfcsb  3864  eqri  3942  nfdisjw  5064  nfdisj  5065  nfopab  5154  nfiotaw  6458  nfiota  6460  nfriota  7336  nfixpw  8864  nfixp  8865  esumnul  34192  hasheuni  34229  dvelimalcasei  35218  dvelimexcasei  35220  wl-cbvalnae  37858  wl-equsal  37866  limsup10ex  46201  liminf10ex  46202  liminfvalxr  46211  liminf0  46221  stowei  46492  ioosshoi  47097  vonioolem2  47109