Theorem nftru 1806

Description: The true constant has no free variables. (This can also be proven in one step with nfv 1915, but this proof does not use ax-5 1911.) (Contributed by Mario Carneiro, 6-Oct-2016.)

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1542	. 2 ⊢ ⊤
2	1	nfth 1803	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1539  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 210  df-tru 1541  df-nf 1786

This theorem is referenced by:  nfsb  2542  nfmov  2619  nfmo  2621  nfeuw  2654  nfeu  2655  dvelimc  2980  nfralw  3189  nfral  3190  nfrex  3268  nfrexg  3269  nfreuw  3327  nfrmow  3328  nfreu  3329  nfrmo  3330  nfrabw  3338  nfrab  3339  rabtru  3625  nfsbcw  3742  nfsbc  3745  nfcsbw  3854  nfcsb  3855  eqri  3935  nfdisjw  5007  nfdisj  5008  nfiotaw  6287  nfiota  6289  nfriota  7105  nfixpw  8463  nfixp  8464  esumnul  31417  hasheuni  31454  wl-cbvalnae  34938  wl-equsal  34945  limsup10ex  42415  liminf10ex  42416  liminfvalxr  42425  liminf0  42435  stowei  42706  ioosshoi  43308  vonioolem2  43320