Theorem nftru 1801

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1541	. 2 ⊢ ⊤
2	1	nfth 1798	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1538  Ⅎwnf 1780

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

This theorem depends on definitions:  df-bi 207  df-tru 1540  df-nf 1781

This theorem is referenced by:  nfsb  2526  nfmov  2558  nfmo  2560  nfeuw  2591  nfeu  2592  dvelimc  2929  nfralwOLD  3310  nfrexw  3311  nfral  3372  nfrex  3373  nfreuwOLD  3423  nfrmowOLD  3424  nfrmo  3431  nfreu  3432  nfrabw  3473  nfrabwOLD  3474  nfrab  3476  rabtru  3692  nfsbcw  3813  nfsbc  3816  nfcsbw  3935  nfcsb  3936  eqri  4016  nfdisjw  5127  nfdisj  5128  nfopab  5217  nfiotaw  6520  nfiota  6522  nfriota  7400  nfixpw  8955  nfixp  8956  esumnul  34029  hasheuni  34066  dvelimalcasei  35069  dvelimexcasei  35071  wl-cbvalnae  37514  wl-equsal  37522  limsup10ex  45729  liminf10ex  45730  liminfvalxr  45739  liminf0  45749  stowei  46020  ioosshoi  46625  vonioolem2  46637