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  2522  nfmov  2554  nfmo  2556  nfeuw  2587  nfeu  2588  dvelimc  2919  nfralwOLD  3289  nfrexw  3290  nfral  3351  nfrex  3352  nfrmo  3409  nfreu  3410  nfrabw  3450  nfrabwOLD  3451  nfrab  3453  rabtru  3664  nfsbcw  3783  nfsbc  3786  nfcsbw  3896  nfcsb  3897  eqri  3975  nfdisjw  5094  nfdisj  5095  nfopab  5184  nfiotaw  6476  nfiota  6478  nfriota  7363  nfixpw  8893  nfixp  8894  esumnul  34046  hasheuni  34083  dvelimalcasei  35074  dvelimexcasei  35076  wl-cbvalnae  37518  wl-equsal  37526  limsup10ex  45744  liminf10ex  45745  liminfvalxr  45754  liminf0  45764  stowei  46035  ioosshoi  46640  vonioolem2  46652