Theorem nftru 1823

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1563	. 2 ⊢ ⊤
2	1	nfth 1820	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1560  Ⅎwnf 1802

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

This theorem depends on definitions:  df-bi 209  df-tru 1562  df-nf 1803

This theorem is referenced by:  nfsb  2553  nfmov  2586  nfmo  2588  nfeuw  2619  nfeu  2620  dvelimc  2948  nfrexw  3309  nfral  3360  nfrex  3361  nfrmo  3411  nfreu  3412  nfrab  3451  rabtru  3647  nfsbcw  3764  nfsbc  3767  nfcsbw  3876  nfcsb  3877  eqri  3954  nfdisjw  5076  nfdisj  5077  nfopab  5166  nfiotaw  6476  nfiota  6478  nfriota  7360  nfixpw  8892  nfixp  8893  esumnul  34306  hasheuni  34343  dvelimalcasei  35332  dvelimexcasei  35334  wl-cbvalnae  37997  wl-equsal  38005  limsup10ex  46308  liminf10ex  46309  liminfvalxr  46318  liminf0  46328  stowei  46599  ioosshoi  47204  vonioolem2  47216