Theorem nftru 1802

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 1541	. 2 ⊢ ⊤
2	1	nfth 1799	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1538  Ⅎwnf 1781

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

This theorem depends on definitions:  df-bi 207  df-tru 1540  df-nf 1782

This theorem is referenced by:  nfsb  2531  nfmov  2563  nfmo  2565  nfeuw  2596  nfeu  2597  dvelimc  2937  nfralwOLD  3318  nfrexw  3319  nfral  3382  nfrex  3383  nfreuwOLD  3433  nfrmowOLD  3434  nfrmo  3441  nfreu  3442  nfrabw  3483  nfrabwOLD  3484  nfrab  3486  rabtru  3705  nfsbcw  3826  nfsbc  3829  nfcsbw  3948  nfcsb  3949  eqri  4029  nfdisjw  5145  nfdisj  5146  nfopab  5235  nfiotaw  6529  nfiota  6531  nfriota  7417  nfixpw  8974  nfixp  8975  esumnul  34012  hasheuni  34049  dvelimalcasei  35052  dvelimexcasei  35054  wl-cbvalnae  37487  wl-equsal  37495  limsup10ex  45694  liminf10ex  45695  liminfvalxr  45704  liminf0  45714  stowei  45985  ioosshoi  46590  vonioolem2  46602