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

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

Proof of Theorem nftru
StepHypRef Expression
1 tru 1511 . 2
21nfth 1764 1 𝑥
Colors of variables: wff setvar class
Syntax hints:  wtru 1508  wnf 1746
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758
This theorem depends on definitions:  df-bi 199  df-tru 1510  df-nf 1747
This theorem is referenced by:  nfmo  2574  nfeu  2613  moexexvw  2662  2moswapv  2663  2mo  2680  nfceqiOLD  2923  dvelimc  2951  nfral  3168  nfrex  3247  nfreu  3309  nfrmo  3310  nfrab  3319  rabtru  3586  nfsbc  3697  nfcsb  3800  nfdisj  4905  reusv1  5147  reusv2lem1  5148  nfiota  6153  nfriota  6944  nfixp  8276  eqri  30026  esumnul  30980  hasheuni  31017  wl-cbvalnae  34244  wl-equsal  34251  limsup10ex  41510  liminf10ex  41511  liminfvalxr  41520  liminf0  41530  stowei  41805  ioosshoi  42407  vonioolem2  42419
  Copyright terms: Public domain W3C validator