Theorem nftru 1836

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1573	. 2 ⊢ ⊤
2	1	nfth 1833	1 ⊢ Ⅎ𝑥⊤

This proof depends on syntax axioms:  ⊤wtru 1570  Ⅎwnf 1815

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

This proof depends on definitions:  df-bi 210  df-tru 1572  df-nf 1816

This theorem is used by:  nfsb  2552  nfmov  2585  nfmo  2587  nfeuw  2618  nfeu  2619  dvelimc  2947  nfrexw  3310  nfral  3359  nfrex  3360  nfrmo  3410  nfreu  3411  nfrab  3448  rabtru  3642  nfsbcw  3760  nfsbc  3763  nfcsbw  3873  nfcsb  3874  eqri  3929  nfdisjw  5081  nfdisj  5082  nfopab  5173  nfiotaw  6500  nfiota  6502  nfriota  7391  nfixpw  8949  nfixp  8950  esumnul  34728  hasheuni  34765  dvelimalcasei  35754  dvelimexcasei  35756  wl-cbvalnae  38572  wl-equsal  38580  limsup10ex  46890  liminf10ex  46891  liminfvalxr  46900  liminf0  46910  stowei  47181  ioosshoi  47786  vonioolem2  47798