Theorem nftru 1799

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1538	. 2 ⊢ ⊤
2	1	nfth 1796	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1535  Ⅎwnf 1778

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

This theorem depends on definitions:  df-bi 206  df-tru 1537  df-nf 1779

This theorem is referenced by:  nfsb  2518  nfmov  2550  nfmo  2552  nfeuw  2583  nfeu  2584  dvelimc  2928  nfralwOLD  3306  nfrexw  3307  nfral  3367  nfrex  3368  nfreuwOLD  3419  nfrmowOLD  3420  nfrmo  3427  nfreu  3428  nfrabw  3465  nfrabwOLD  3466  nfrab  3469  rabtru  3679  nfsbcw  3798  nfsbc  3801  nfcsbw  3919  nfcsb  3920  eqri  4000  nfdisjw  5125  nfdisj  5126  nfopab  5217  nfiotaw  6504  nfiota  6506  nfriota  7389  nfixpw  8935  nfixp  8936  esumnul  33667  hasheuni  33704  wl-cbvalnae  37000  wl-equsal  37008  limsup10ex  45161  liminf10ex  45162  liminfvalxr  45171  liminf0  45181  stowei  45452  ioosshoi  46057  vonioolem2  46069