Theorem nftru 1807

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1546	. 2 ⊢ ⊤
2	1	nfth 1804	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1543  Ⅎwnf 1786

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

This theorem depends on definitions:  df-bi 206  df-tru 1545  df-nf 1787

This theorem is referenced by:  nfsb  2523  nfmov  2555  nfmo  2557  nfeuw  2588  nfeu  2589  dvelimc  2932  nfralwOLD  3310  nfrexw  3311  nfral  3371  nfrex  3372  nfreuwOLD  3423  nfrmowOLD  3424  nfrmo  3431  nfreu  3432  nfrabw  3469  nfrabwOLD  3470  nfrab  3473  rabtru  3681  nfsbcw  3800  nfsbc  3803  nfcsbw  3921  nfcsb  3922  eqri  4003  nfdisjw  5126  nfdisj  5127  nfopab  5218  nfiotaw  6500  nfiota  6502  nfriota  7378  nfixpw  8910  nfixp  8911  esumnul  33046  hasheuni  33083  wl-cbvalnae  36402  wl-equsal  36409  limsup10ex  44489  liminf10ex  44490  liminfvalxr  44499  liminf0  44509  stowei  44780  ioosshoi  45385  vonioolem2  45397