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

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

Proof of Theorem nftru
StepHypRef Expression
1 tru 1327 . 2  |-  T.
21nfth 1559 1  |-  F/ x  T.
Colors of variables: wff set class
Syntax hints:    T. wtru 1322   F/wnf 1550
This theorem is referenced by:  sbie  2071  nfeu  2254  nfmo  2255  dvelimc  2544  nfral  2702  nfreu  2825  nfrmo  2826  nfrab  2832  nfsbc  3125  nfcsb  3228  nfdisj  4135  nfiota  5362  nfriota  6495  nfixp  7017  eqri  23838  esumnul  24239  hasheuni  24271  stowei  27481  sbieNEW7  28877
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552
This theorem depends on definitions:  df-bi 178  df-tru 1325  df-nf 1551
  Copyright terms: Public domain W3C validator