Theorem nftru 1806

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1545	. 2 ⊢ ⊤
2	1	nfth 1803	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1542  Ⅎ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 206  df-tru 1544  df-nf 1786

This theorem is referenced by:  nfsb  2521  nfmov  2553  nfmo  2555  nfeuw  2586  nfeu  2587  dvelimc  2930  nfralwOLD  3293  nfrexw  3294  nfral  3345  nfrex  3346  nfreuwOLD  3395  nfrmowOLD  3396  nfrmo  3403  nfreu  3404  nfrabw  3441  nfrabwOLD  3442  nfrab  3444  rabtru  3645  nfsbcw  3764  nfsbc  3767  nfcsbw  3885  nfcsb  3886  eqri  3967  nfdisjw  5087  nfdisj  5088  nfopab  5179  nfiotaw  6457  nfiota  6459  nfriota  7331  nfixpw  8861  nfixp  8862  esumnul  32736  hasheuni  32773  wl-cbvalnae  36065  wl-equsal  36072  limsup10ex  44134  liminf10ex  44135  liminfvalxr  44144  liminf0  44154  stowei  44425  ioosshoi  45030  vonioolem2  45042