Theorem nftru 1837

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1574	. 2 ⊢ ⊤
2	1	nfth 1834	1 ⊢ Ⅎ𝑥⊤

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-tru 1573  df-nf 1817

This theorem is used by:  nfsb  2553  nfmov  2586  nfmo  2588  nfeuw  2619  nfeu  2620  dvelimc  2948  nfrexw  3311  nfral  3360  nfrex  3361  nfrmo  3411  nfreu  3412  nfrab  3449  rabtru  3643  nfsbcw  3761  nfsbc  3764  nfcsbw  3873  nfcsb  3874  eqri  3951  nfdisjw  5082  nfdisj  5083  nfopab  5174  nfiotaw  6497  nfiota  6499  nfriota  7387  nfixpw  8937  nfixp  8938  esumnul  34673  hasheuni  34710  dvelimalcasei  35699  dvelimexcasei  35701  wl-cbvalnae  38445  wl-equsal  38453  limsup10ex  46752  liminf10ex  46753  liminfvalxr  46762  liminf0  46772  stowei  47043  ioosshoi  47648  vonioolem2  47660