Theorem nftru 1803

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1543	. 2 ⊢ ⊤
2	1	nfth 1800	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1540  Ⅎwnf 1782

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

This theorem depends on definitions:  df-bi 207  df-tru 1542  df-nf 1783

This theorem is referenced by:  nfsb  2526  nfmov  2558  nfmo  2560  nfeuw  2591  nfeu  2592  dvelimc  2923  nfralwOLD  3296  nfrexw  3297  nfral  3358  nfrex  3359  nfreuwOLD  3410  nfrmowOLD  3411  nfrmo  3418  nfreu  3419  nfrabw  3459  nfrabwOLD  3460  nfrab  3462  rabtru  3673  nfsbcw  3794  nfsbc  3797  nfcsbw  3907  nfcsb  3908  eqri  3986  nfdisjw  5104  nfdisj  5105  nfopab  5194  nfiotaw  6499  nfiota  6501  nfriota  7383  nfixpw  8939  nfixp  8940  esumnul  33990  hasheuni  34027  dvelimalcasei  35031  dvelimexcasei  35033  wl-cbvalnae  37475  wl-equsal  37483  limsup10ex  45733  liminf10ex  45734  liminfvalxr  45743  liminf0  45753  stowei  46024  ioosshoi  46629  vonioolem2  46641