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 1540	. 2 ⊢ ⊤
2	1	nfth 1801	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1537  Ⅎ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 209  df-tru 1539  df-nf 1784

This theorem is referenced by:  nfsb  2564  nfmov  2643  nfmo  2645  nfeuw  2678  nfeu  2679  nfceqiOLD  2977  dvelimc  3009  nfralw  3228  nfral  3229  nfrex  3312  nfrexg  3313  nfreuw  3377  nfrmow  3378  nfreu  3379  nfrmo  3380  nfrabw  3388  nfrab  3389  rabtru  3680  nfsbcw  3797  nfsbc  3800  nfcsbw  3912  nfcsb  3913  eqri  3990  nfdisjw  5046  nfdisj  5047  nfiotaw  6321  nfiota  6323  nfriota  7129  nfixpw  8483  nfixp  8484  esumnul  31311  hasheuni  31348  wl-cbvalnae  34777  wl-equsal  34784  limsup10ex  42060  liminf10ex  42061  liminfvalxr  42070  liminf0  42080  stowei  42356  ioosshoi  42958  vonioolem2  42970