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  2528  nfmov  2561  nfmo  2563  nfeuw  2594  nfeu  2595  dvelimc  2925  nfrexw  3286  nfral  3346  nfrex  3347  nfrmo  3399  nfreu  3400  nfrabw  3438  nfrab  3440  rabtru  3646  nfsbcw  3764  nfsbc  3767  nfcsbw  3877  nfcsb  3878  eqri  3956  nfdisjw  5079  nfdisj  5080  nfopab  5169  nfiotaw  6460  nfiota  6462  nfriota  7337  nfixpw  8866  nfixp  8867  esumnul  34226  hasheuni  34263  dvelimalcasei  35252  dvelimexcasei  35254  wl-cbvalnae  37788  wl-equsal  37796  limsup10ex  46131  liminf10ex  46132  liminfvalxr  46141  liminf0  46151  stowei  46422  ioosshoi  47027  vonioolem2  47039