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  2527  nfmov  2560  nfmo  2562  nfeuw  2593  nfeu  2594  dvelimc  2924  nfrexw  3284  nfral  3344  nfrex  3345  nfrmo  3397  nfreu  3398  nfrabw  3436  nfrab  3438  rabtru  3644  nfsbcw  3762  nfsbc  3765  nfcsbw  3875  nfcsb  3876  eqri  3954  nfdisjw  5077  nfdisj  5078  nfopab  5167  nfiotaw  6452  nfiota  6454  nfriota  7327  nfixpw  8854  nfixp  8855  esumnul  34205  hasheuni  34242  dvelimalcasei  35232  dvelimexcasei  35234  wl-cbvalnae  37738  wl-equsal  37746  limsup10ex  46017  liminf10ex  46018  liminfvalxr  46027  liminf0  46037  stowei  46308  ioosshoi  46913  vonioolem2  46925