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

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

Proof of Theorem nftru
StepHypRef Expression
1 tru 1402 . 2  |- T.
21nfth 1630 1  |-  F/ x T.
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1399   F/wnf 1621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623
This theorem depends on definitions:  df-bi 185  df-tru 1401  df-nf 1622
This theorem is referenced by:  nfeu  2302  nfmo  2303  nfceqi  2612  dvelimc  2640  nfral  2840  nfrex  2917  nfreu  3029  nfrmo  3030  nfrab  3036  nfsbc  3346  nfcsb  3438  nfdisj  4422  nfiota  5538  nfriota  6241  nfixp  7481  rabtru  27601  eqri  27613  esumnul  28280  hasheuni  28317  wl-cbvalnae  30229  wl-equsal  30236  dvtanlem  30307  stowei  32088
  Copyright terms: Public domain W3C validator