Theorem nftru 1805

Description: The true constant has no free variables. (This can also be proven in one step with nfv 1915, but this proof does not use ax-5 1911.) (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 1802	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1542  Ⅎwnf 1784

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

This theorem depends on definitions:  df-bi 207  df-tru 1544  df-nf 1785

This theorem is referenced by:  nfsb  2525  nfmov  2557  nfmo  2559  nfeuw  2590  nfeu  2591  dvelimc  2921  nfrexw  3281  nfral  3341  nfrex  3342  nfrmo  3394  nfreu  3395  nfrabw  3433  nfrab  3435  rabtru  3641  nfsbcw  3759  nfsbc  3762  nfcsbw  3872  nfcsb  3873  eqri  3951  nfdisjw  5074  nfdisj  5075  nfopab  5164  nfiotaw  6449  nfiota  6451  nfriota  7324  nfixpw  8850  nfixp  8851  esumnul  34133  hasheuni  34170  dvelimalcasei  35160  dvelimexcasei  35162  wl-cbvalnae  37650  wl-equsal  37658  limsup10ex  45933  liminf10ex  45934  liminfvalxr  45943  liminf0  45953  stowei  46224  ioosshoi  46829  vonioolem2  46841