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  2523  nfmov  2555  nfmo  2557  nfeuw  2588  nfeu  2589  dvelimc  2920  nfrexw  3280  nfral  3340  nfrex  3341  nfrmo  3393  nfreu  3394  nfrabw  3432  nfrab  3434  rabtru  3640  nfsbcw  3758  nfsbc  3761  nfcsbw  3871  nfcsb  3872  eqri  3950  nfdisjw  5065  nfdisj  5066  nfopab  5155  nfiotaw  6436  nfiota  6438  nfriota  7310  nfixpw  8835  nfixp  8836  esumnul  34053  hasheuni  34090  dvelimalcasei  35080  dvelimexcasei  35082  wl-cbvalnae  37567  wl-equsal  37575  limsup10ex  45811  liminf10ex  45812  liminfvalxr  45821  liminf0  45831  stowei  46102  ioosshoi  46707  vonioolem2  46719