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

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

Proof of Theorem nftru
StepHypRef Expression
1 tru 1312 . 2  |-  T.
21nfth 1543 1  |-  F/ x  T.
Colors of variables: wff set class
Syntax hints:    T. wtru 1307   F/wnf 1534
This theorem is referenced by:  sbie  1991  nfeu  2172  nfmo  2173  dvelimc  2453  nfral  2609  nfreu  2727  nfrmo  2728  nfrab  2734  nfsbc  3025  nfcsb  3128  nfdisj  4021  nfiota  5239  nfriota  6330  nfixp  6851  eqri  23203  esumnul  23442  hasheuni  23468  stowei  27916  stirlinglem13  27938  sbieNEW7  29516
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536
This theorem depends on definitions:  df-bi 177  df-tru 1310  df-nf 1535
  Copyright terms: Public domain W3C validator