Theorem nftru 1811

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1551	. 2 ⊢ ⊤
2	1	nfth 1808	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1548  Ⅎwnf 1790

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

This theorem depends on definitions:  df-bi 208  df-tru 1550  df-nf 1791

This theorem is referenced by:  nfsb  2531  nfmov  2564  nfmo  2566  nfeuw  2597  nfeu  2598  dvelimc  2926  nfrexw  3287  nfral  3338  nfrex  3339  nfrmo  3389  nfreu  3390  nfrab  3429  rabtru  3627  nfsbcw  3745  nfsbc  3748  nfcsbw  3857  nfcsb  3858  eqri  3935  nfdisjw  5051  nfdisj  5052  nfopab  5141  nfiotaw  6445  nfiota  6447  nfriota  7325  nfixpw  8854  nfixp  8855  esumnul  34232  hasheuni  34269  dvelimalcasei  35258  dvelimexcasei  35260  wl-cbvalnae  37904  wl-equsal  37912  limsup10ex  46216  liminf10ex  46217  liminfvalxr  46226  liminf0  46236  stowei  46507  ioosshoi  47112  vonioolem2  47124