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

Theorem nftru 1677
Description: The true constant has no free variables. (This can also be proven in one step with nfv 1761, but this proof does not use ax-5 1758.) (Contributed by Mario Carneiro, 6-Oct-2016.)
Assertion
Ref Expression
nftru  |-  F/ x T.

Proof of Theorem nftru
StepHypRef Expression
1 tru 1448 . 2  |- T.
21nfth 1676 1  |-  F/ x T.
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1445   F/wnf 1667
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669
This theorem depends on definitions:  df-bi 189  df-tru 1447  df-nf 1668
This theorem is referenced by:  nfeu  2315  nfmo  2316  nfceqi  2589  dvelimc  2614  nfral  2774  nfrex  2850  nfreu  2965  nfrmo  2966  nfrab  2972  nfsbc  3289  nfcsb  3381  nfdisj  4385  nfiota  5550  nfriota  6261  nfixp  7541  rabtru  28135  eqri  28147  esumnul  28869  hasheuni  28906  wl-cbvalnae  31866  wl-equsal  31873  dvtanlemOLD  31991  stowei  37926
  Copyright terms: Public domain W3C validator