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

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

Proof of Theorem nftru
StepHypRef Expression
1 tru 1635 . 2
21nfth 1875 1 𝑥
Colors of variables: wff setvar class
Syntax hints:  wtru 1632  wnf 1856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870
This theorem depends on definitions:  df-bi 197  df-tru 1634  df-nf 1858
This theorem is referenced by:  nfeu  2634  nfmo  2635  nfceqi  2910  dvelimc  2936  nfral  3094  nfrex  3155  nfreu  3262  nfrmo  3263  nfrab  3272  rabtru  3512  nfsbc  3609  nfcsb  3700  nfdisj  4766  nfiota  5998  nfriota  6763  nfixp  8081  eqri  29655  esumnul  30450  hasheuni  30487  wl-cbvalnae  33655  wl-equsal  33661  limsup10ex  40523  liminf10ex  40524  liminfvalxr  40533  liminf0  40543  stowei  40798  ioosshoi  41403  vonioolem2  41415
  Copyright terms: Public domain W3C validator