Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nftru Structured version   Visualization version   GIF version

Theorem nftru 1806
 Description: The true constant has no free variables. (This can also be proven in one step with nfv 1915, but this proof does not use ax-5 1911.) (Contributed by Mario Carneiro, 6-Oct-2016.)
Assertion
Ref Expression
nftru 𝑥

Proof of Theorem nftru
StepHypRef Expression
1 tru 1542 . 2
21nfth 1803 1 𝑥
 Colors of variables: wff setvar class Syntax hints:  ⊤wtru 1539  Ⅎwnf 1785 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797 This theorem depends on definitions:  df-bi 210  df-tru 1541  df-nf 1786 This theorem is referenced by:  nfsb  2565  nfmov  2643  nfmo  2645  nfeuw  2678  nfeu  2679  dvelimc  3004  nfralw  3214  nfral  3215  nfrex  3295  nfrexg  3296  nfreuw  3355  nfrmow  3356  nfreu  3357  nfrmo  3358  nfrabw  3366  nfrab  3367  rabtru  3652  nfsbcw  3769  nfsbc  3772  nfcsbw  3881  nfcsb  3882  eqri  3962  nfdisjw  5019  nfdisj  5020  nfiotaw  6297  nfiota  6299  nfriota  7110  nfixpw  8467  nfixp  8468  esumnul  31381  hasheuni  31418  wl-cbvalnae  34896  wl-equsal  34903  limsup10ex  42354  liminf10ex  42355  liminfvalxr  42364  liminf0  42374  stowei  42645  ioosshoi  43247  vonioolem2  43259
 Copyright terms: Public domain W3C validator