Theorem nftru 1837

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1574	. 2 ⊢ ⊤
2	1	nfth 1834	1 ⊢ Ⅎ𝑥⊤

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-tru 1573  df-nf 1817

This theorem is used by:  nfsb  2555  nfmov  2588  nfmo  2590  nfeuw  2621  nfeu  2622  dvelimc  2951  nfrexw  3314  nfral  3363  nfrex  3364  nfrmo  3414  nfreu  3415  nfrab  3452  rabtru  3646  nfsbcw  3764  nfsbc  3767  nfcsbw  3877  nfcsb  3878  eqri  3933  nfdisjw  5087  nfdisj  5088  nfopab  5180  nfiotaw  6524  nfiota  6526  nfriota  7420  nfixpw  8982  nfixp  8983  esumnul  34791  hasheuni  34828  dvelimalcasei  35817  dvelimexcasei  35819  wl-cbvalnae  38733  wl-equsal  38741  limsup10ex  47056  liminf10ex  47057  liminfvalxr  47066  liminf0  47076  stowei  47347  ioosshoi  47952  vonioolem2  47964