Theorem nftru 1721

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

Assertion

Ref	Expression
nftru	⊢ Ⅎ𝑥⊤

Proof of Theorem nftru

Step	Hyp	Ref	Expression
1		tru 1479	. 2 ⊢ ⊤
2	1	nfth 1718	1 ⊢ Ⅎ𝑥⊤

Syntax hints:  ⊤wtru 1476  Ⅎwnf 1699

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

This theorem depends on definitions:  df-bi 196  df-tru 1478  df-nf 1701

This theorem is referenced by:  nfeu  2474  nfmo  2475  nfceqi  2748  dvelimc  2773  nfral  2929  nfrex  2990  nfreu  3093  nfrmo  3094  nfrab  3100  nfsbc  3424  nfcsb  3517  nfdisj  4565  nfiota  5772  nfriota  6520  nfixp  7813  rabtru  28723  eqri  28735  esumnul  29437  hasheuni  29474  wl-cbvalnae  32499  wl-equsal  32505  stowei  38957  ioosshoi  39560  vonioolem2  39572