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

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

Proof of Theorem nftru
StepHypRef Expression
1 tru 1399 . 2
21nfth 1625 1
Colors of variables: wff setvar class
Syntax hints:   wtru 1396  F/wnf 1616
This theorem is referenced by:  nfeu  2300  nfmo  2301  nfceqi  2615  dvelimc  2643  nfral  2843  nfrex  2920  nfreu  3032  nfrmo  3033  nfrab  3039  nfsbc  3349  nfcsb  3452  nfdisj  4434  nfiota  5560  nfriota  6266  nfixp  7508  eqri  27411  esumnul  28059  hasheuni  28091  wl-cbvalnae  29986  wl-equsal  29993  dvtanlem  30064  stowei  31846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618
This theorem depends on definitions:  df-bi 185  df-tru 1398  df-nf 1617
  Copyright terms: Public domain W3C validator