Theorem nftru 1767

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1511	. 2 ⊢ ⊤
2	1	nfth 1764	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1508  Ⅎwnf 1746

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

This theorem depends on definitions:  df-bi 199  df-tru 1510  df-nf 1747

This theorem is referenced by:  nfmo  2574  nfeu  2613  moexexvw  2662  2moswapv  2663  2mo  2680  nfceqiOLD  2923  dvelimc  2951  nfral  3168  nfrex  3247  nfreu  3309  nfrmo  3310  nfrab  3319  rabtru  3586  nfsbc  3697  nfcsb  3800  nfdisj  4905  reusv1  5147  reusv2lem1  5148  nfiota  6153  nfriota  6944  nfixp  8276  eqri  30026  esumnul  30980  hasheuni  31017  wl-cbvalnae  34244  wl-equsal  34251  limsup10ex  41510  liminf10ex  41511  liminfvalxr  41520  liminf0  41530  stowei  41805  ioosshoi  42407  vonioolem2  42419