Theorem nftru 1834

Description: The true constant has no free variables. (This can also be proven in one step with nfv 1944, but this proof does not use ax-5 1940.) (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 1831	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1571  Ⅎwnf 1813

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

This theorem depends on definitions:  df-bi 210  df-tru 1573  df-nf 1814

This theorem is referenced by:  nfsb  2555  nfmov  2588  nfmo  2590  nfeuw  2621  nfeu  2622  dvelimc  2950  nfrexw  3313  nfral  3363  nfrex  3364  nfrmo  3414  nfreu  3415  nfrab  3453  rabtru  3648  nfsbcw  3766  nfsbc  3769  nfcsbw  3879  nfcsb  3880  eqri  3957  nfdisjw  5088  nfdisj  5089  nfopab  5180  nfiotaw  6496  nfiota  6498  nfriota  7379  nfixpw  8910  nfixp  8911  esumnul  34438  hasheuni  34475  dvelimalcasei  35464  dvelimexcasei  35466  wl-cbvalnae  38188  wl-equsal  38196  limsup10ex  46487  liminf10ex  46488  liminfvalxr  46497  liminf0  46507  stowei  46778  ioosshoi  47383  vonioolem2  47395