Theorem nftru 1837

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1574	. 2 ⊢ ⊤
2	1	nfth 1834	1 ⊢ Ⅎ𝑥⊤

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-tru 1573  df-nf 1817

This theorem is used by:  nfsb  2557  nfmov  2590  nfmo  2592  nfeuw  2623  nfeu  2624  dvelimc  2952  nfrexw  3315  nfral  3365  nfrex  3366  nfrmo  3416  nfreu  3417  nfrab  3455  rabtru  3650  nfsbcw  3768  nfsbc  3771  nfcsbw  3880  nfcsb  3881  eqri  3958  nfdisjw  5090  nfdisj  5091  nfopab  5182  nfiotaw  6500  nfiota  6502  nfriota  7388  nfixpw  8920  nfixp  8921  esumnul  34502  hasheuni  34539  dvelimalcasei  35529  dvelimexcasei  35531  wl-cbvalnae  38245  wl-equsal  38253  limsup10ex  46545  liminf10ex  46546  liminfvalxr  46555  liminf0  46565  stowei  46836  ioosshoi  47441  vonioolem2  47453