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

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

Proof of Theorem nftru
StepHypRef Expression
1 tru 1527 . 2
21nfth 1767 1 𝑥
Colors of variables: wff setvar class
Syntax hints:  wtru 1524  wnf 1748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762
This theorem depends on definitions:  df-bi 197  df-tru 1526  df-nf 1750
This theorem is referenced by:  nfeu  2514  nfmo  2515  nfceqi  2790  dvelimc  2816  nfral  2974  nfrex  3036  nfreu  3143  nfrmo  3144  nfrab  3153  rabtru  3393  nfsbc  3490  nfcsb  3584  nfdisj  4664  nfiota  5893  nfriota  6660  nfixp  7969  eqri  29443  esumnul  30238  hasheuni  30275  wl-cbvalnae  33450  wl-equsal  33456  limsup10ex  40323  liminf10ex  40324  liminfvalxr  40333  liminf0  40343  stowei  40599  ioosshoi  41204  vonioolem2  41216
  Copyright terms: Public domain W3C validator