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

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

Proof of Theorem nftru
StepHypRef Expression
1 tru 1374 . 2  |- T.
21nfth 1599 1  |-  F/ x T.
Colors of variables: wff setvar class
Syntax hints:   T. wtru 1371   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592
This theorem depends on definitions:  df-bi 185  df-tru 1373  df-nf 1591
This theorem is referenced by:  nfeu  2280  nfmo  2281  nfceqi  2610  dvelimc  2637  nfral  2882  nfreu  2995  nfrmo  2996  nfrab  3002  nfsbc  3310  nfcsb  3408  nfdisj  4377  nfiota  5488  nfriota  6165  nfixp  7387  eqri  26041  esumnul  26642  hasheuni  26674  wl-cbvalnae  28505  wl-equsal  28512  dvtanlem  28584  stowei  30002
  Copyright terms: Public domain W3C validator