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

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

Proof of Theorem nftru
StepHypRef Expression
1 tru 1478 . 2
21nfth 1717 1 𝑥
Colors of variables: wff setvar class
Syntax hints:  wtru 1475  wnf 1698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712
This theorem depends on definitions:  df-bi 195  df-tru 1477  df-nf 1700
This theorem is referenced by:  nfeu  2473  nfmo  2474  nfceqi  2747  dvelimc  2772  nfral  2928  nfrex  2989  nfreu  3092  nfrmo  3093  nfrab  3099  nfsbc  3423  nfcsb  3516  nfdisj  4559  nfiota  5758  nfriota  6498  nfixp  7790  rabtru  28529  eqri  28541  esumnul  29243  hasheuni  29280  wl-cbvalnae  32295  wl-equsal  32301  stowei  38754  ioosshoi  39357  vonioolem2  39369
  Copyright terms: Public domain W3C validator