Theorem nftru 1831

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1571	. 2 ⊢ ⊤
2	1	nfth 1828	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1568  Ⅎwnf 1810

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

This theorem depends on definitions:  df-bi 210  df-tru 1570  df-nf 1811

This theorem is referenced by:  nfsb  2561  nfmov  2594  nfmo  2596  nfeuw  2627  nfeu  2628  dvelimc  2956  nfrexw  3319  nfral  3370  nfrex  3371  nfrmo  3421  nfreu  3422  nfrab  3461  rabtru  3657  nfsbcw  3775  nfsbc  3778  nfcsbw  3887  nfcsb  3888  eqri  3965  nfdisjw  5089  nfdisj  5090  nfopab  5181  nfiotaw  6494  nfiota  6496  nfriota  7377  nfixpw  8910  nfixp  8911  esumnul  34379  hasheuni  34416  dvelimalcasei  35405  dvelimexcasei  35407  wl-cbvalnae  38071  wl-equsal  38079  limsup10ex  46374  liminf10ex  46375  liminfvalxr  46384  liminf0  46394  stowei  46665  ioosshoi  47270  vonioolem2  47282