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  2521  nfmov  2553  nfmo  2555  nfeuw  2586  nfeu  2587  dvelimc  2917  nfrexw  3278  nfral  3339  nfrex  3340  nfrmo  3394  nfreu  3395  nfrabw  3434  nfrab  3436  rabtru  3647  nfsbcw  3766  nfsbc  3769  nfcsbw  3879  nfcsb  3880  eqri  3958  nfdisjw  5074  nfdisj  5075  nfopab  5164  nfiotaw  6446  nfiota  6448  nfriota  7322  nfixpw  8850  nfixp  8851  esumnul  34034  hasheuni  34071  dvelimalcasei  35062  dvelimexcasei  35064  wl-cbvalnae  37526  wl-equsal  37534  limsup10ex  45774  liminf10ex  45775  liminfvalxr  45784  liminf0  45794  stowei  46065  ioosshoi  46670  vonioolem2  46682