Theorem nftru 1807

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 1804	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1540  Ⅎwnf 1786

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

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

This theorem is referenced by:  nfsb  2528  nfmov  2561  nfmo  2563  nfeuw  2594  nfeu  2595  dvelimc  2936  nfralwOLD  3153  nfral  3154  nfrex  3243  nfrexg  3244  nfreuwOLD  3307  nfrmowOLD  3308  nfreu  3309  nfrmo  3310  nfrabw  3319  nfrabwOLD  3320  nfrab  3321  rabtru  3622  nfsbcw  3739  nfsbc  3742  nfcsbw  3860  nfcsb  3861  eqri  3942  nfdisjw  5052  nfdisj  5053  nfopab  5144  nfiotaw  6399  nfiota  6401  nfriota  7254  nfixpw  8713  nfixp  8714  esumnul  32025  hasheuni  32062  wl-cbvalnae  35701  wl-equsal  35708  limsup10ex  43321  liminf10ex  43322  liminfvalxr  43331  liminf0  43341  stowei  43612  ioosshoi  44214  vonioolem2  44226