Theorem nftru 1804

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1544	. 2 ⊢ ⊤
2	1	nfth 1801	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-tru 1543  df-nf 1784

This theorem is referenced by:  nfsb  2521  nfmov  2553  nfmo  2555  nfeuw  2586  nfeu  2587  dvelimc  2917  nfrexw  3284  nfral  3345  nfrex  3346  nfrmo  3400  nfreu  3401  nfrabw  3440  nfrab  3442  rabtru  3653  nfsbcw  3772  nfsbc  3775  nfcsbw  3885  nfcsb  3886  eqri  3964  nfdisjw  5081  nfdisj  5082  nfopab  5171  nfiotaw  6456  nfiota  6458  nfriota  7338  nfixpw  8866  nfixp  8867  esumnul  34011  hasheuni  34048  dvelimalcasei  35039  dvelimexcasei  35041  wl-cbvalnae  37494  wl-equsal  37502  limsup10ex  45744  liminf10ex  45745  liminfvalxr  45754  liminf0  45764  stowei  46035  ioosshoi  46640  vonioolem2  46652