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  3337  nfrex  3338  nfrmo  3388  nfreu  3389  nfrab  3428  rabtru  3633  nfsbcw  3751  nfsbc  3754  nfcsbw  3864  nfcsb  3865  eqri  3943  nfdisjw  5065  nfdisj  5066  nfopab  5155  nfiotaw  6452  nfiota  6454  nfriota  7329  nfixpw  8857  nfixp  8858  esumnul  34208  hasheuni  34245  dvelimalcasei  35234  dvelimexcasei  35236  wl-cbvalnae  37872  wl-equsal  37880  limsup10ex  46219  liminf10ex  46220  liminfvalxr  46229  liminf0  46239  stowei  46510  ioosshoi  47115  vonioolem2  47127