Theorem nftru 1808

Description: The true constant has no free variables. (This can also be proven in one step with nfv 1918, but this proof does not use ax-5 1914.) (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 1805	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1540  Ⅎwnf 1787

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

This theorem depends on definitions:  df-bi 206  df-tru 1542  df-nf 1788

This theorem is referenced by:  nfsb  2527  nfmov  2560  nfmo  2562  nfeuw  2593  nfeu  2594  dvelimc  2934  nfralw  3149  nfral  3150  nfrex  3237  nfrexg  3238  nfreuw  3300  nfrmow  3301  nfreu  3302  nfrmo  3303  nfrabw  3311  nfrab  3312  rabtru  3614  nfsbcw  3733  nfsbc  3736  nfcsbw  3855  nfcsb  3856  eqri  3937  nfdisjw  5047  nfdisj  5048  nfopab  5139  nfiotaw  6380  nfiota  6382  nfriota  7225  nfixpw  8662  nfixp  8663  esumnul  31916  hasheuni  31953  wl-cbvalnae  35619  wl-equsal  35626  limsup10ex  43204  liminf10ex  43205  liminfvalxr  43214  liminf0  43224  stowei  43495  ioosshoi  44097  vonioolem2  44109