Theorem nftru 1804

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1544	. 2 ⊢ ⊤
2	1	nfth 1801	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1541  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-tru 1543  df-nf 1784

This theorem is referenced by:  nfsb  2521  nfmov  2553  nfmo  2555  nfeuw  2586  nfeu  2587  dvelimc  2917  nfralwOLD  3286  nfrexw  3287  nfral  3348  nfrex  3349  nfrmo  3403  nfreu  3404  nfrabw  3443  nfrab  3445  rabtru  3656  nfsbcw  3775  nfsbc  3778  nfcsbw  3888  nfcsb  3889  eqri  3967  nfdisjw  5086  nfdisj  5087  nfopab  5176  nfiotaw  6468  nfiota  6470  nfriota  7356  nfixpw  8889  nfixp  8890  esumnul  34038  hasheuni  34075  dvelimalcasei  35066  dvelimexcasei  35068  wl-cbvalnae  37521  wl-equsal  37529  limsup10ex  45771  liminf10ex  45772  liminfvalxr  45781  liminf0  45791  stowei  46062  ioosshoi  46667  vonioolem2  46679