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

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

Proof of Theorem nftru
StepHypRef Expression
1 tru 1538 . 2
21nfth 1796 1 𝑥
Colors of variables: wff setvar class
Syntax hints:  wtru 1535  wnf 1778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790
This theorem depends on definitions:  df-bi 206  df-tru 1537  df-nf 1779
This theorem is referenced by:  nfsb  2518  nfmov  2550  nfmo  2552  nfeuw  2583  nfeu  2584  dvelimc  2928  nfralwOLD  3306  nfrexw  3307  nfral  3367  nfrex  3368  nfreuwOLD  3419  nfrmowOLD  3420  nfrmo  3427  nfreu  3428  nfrabw  3465  nfrabwOLD  3466  nfrab  3469  rabtru  3679  nfsbcw  3798  nfsbc  3801  nfcsbw  3919  nfcsb  3920  eqri  4000  nfdisjw  5125  nfdisj  5126  nfopab  5217  nfiotaw  6504  nfiota  6506  nfriota  7389  nfixpw  8935  nfixp  8936  esumnul  33667  hasheuni  33704  wl-cbvalnae  37000  wl-equsal  37008  limsup10ex  45161  liminf10ex  45162  liminfvalxr  45171  liminf0  45181  stowei  45452  ioosshoi  46057  vonioolem2  46069
  Copyright terms: Public domain W3C validator