Theorem nftru 1804

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1544	. 2 ⊢ ⊤
2	1	nfth 1801	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-tru 1543  df-nf 1784

This theorem is referenced by:  nfsb  2527  nfmov  2559  nfmo  2561  nfeuw  2592  nfeu  2593  dvelimc  2924  nfralwOLD  3292  nfrexw  3293  nfral  3353  nfrex  3354  nfreuwOLD  3405  nfrmowOLD  3406  nfrmo  3413  nfreu  3414  nfrabw  3454  nfrabwOLD  3455  nfrab  3457  rabtru  3668  nfsbcw  3787  nfsbc  3790  nfcsbw  3900  nfcsb  3901  eqri  3979  nfdisjw  5098  nfdisj  5099  nfopab  5188  nfiotaw  6487  nfiota  6489  nfriota  7372  nfixpw  8928  nfixp  8929  esumnul  34025  hasheuni  34062  dvelimalcasei  35053  dvelimexcasei  35055  wl-cbvalnae  37497  wl-equsal  37505  limsup10ex  45750  liminf10ex  45751  liminfvalxr  45760  liminf0  45770  stowei  46041  ioosshoi  46646  vonioolem2  46658