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

Theorem nftru 1541
Description: The true constant has no free variables. (This can also be proven in one step with nfv 1605, but this proof does not use ax-17 1603.) (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 1540 1  |-  F/ x  T.
Colors of variables: wff set class
Syntax hints:    T. wtru 1307   F/wnf 1531
This theorem is referenced by:  sbie  1978  nfeu  2159  nfmo  2160  dvelimc  2440  nfral  2596  nfreu  2714  nfrmo  2715  nfrab  2721  nfsbc  3012  nfcsb  3115  nfdisj  4005  nfiota  5223  nfriota  6314  nfixp  6835  eqri  23187  esumnul  23427  hasheuni  23453  stowei  27813  stirlinglem13  27835
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533
This theorem depends on definitions:  df-bi 177  df-tru 1310  df-nf 1532
  Copyright terms: Public domain W3C validator