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  2552  nfmov  2585  nfmo  2587  nfeuw  2618  nfeu  2619  dvelimc  2947  nfrexw  3310  nfral  3359  nfrex  3360  nfrmo  3410  nfreu  3411  nfrab  3448  rabtru  3643  nfsbcw  3761  nfsbc  3764  nfcsbw  3873  nfcsb  3874  eqri  3951  nfdisjw  5082  nfdisj  5083  nfopab  5174  nfiotaw  6493  nfiota  6495  nfriota  7382  nfixpw  8923  nfixp  8924  esumnul  34558  hasheuni  34595  dvelimalcasei  35585  dvelimexcasei  35587  wl-cbvalnae  38296  wl-equsal  38304  limsup10ex  46601  liminf10ex  46602  liminfvalxr  46611  liminf0  46621  stowei  46892  ioosshoi  47497  vonioolem2  47509