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

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

Proof of Theorem nftru
StepHypRef Expression
1 tru 1330 . 2  |-  T.
21nfth 1562 1  |-  F/ x  T.
Colors of variables: wff set class
Syntax hints:    T. wtru 1325   F/wnf 1553
This theorem is referenced by:  sbieOLD  2125  nfeu  2296  nfmo  2297  dvelimc  2592  nfral  2751  nfreu  2874  nfrmo  2875  nfrab  2881  nfsbc  3174  nfcsb  3277  nfdisj  4186  nfiota  5414  nfriota  6551  nfixp  7073  eqri  23986  esumnul  24435  hasheuni  24467  stowei  27780  sbieNEW7  29478
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555
This theorem depends on definitions:  df-bi 178  df-tru 1328  df-nf 1554
  Copyright terms: Public domain W3C validator