![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nftru | Structured version Visualization version GIF version |
Description: The true constant has no free variables. (This can also be proven in one step with nfv 1873, but this proof does not use ax-5 1869.) (Contributed by Mario Carneiro, 6-Oct-2016.) |
Ref | Expression |
---|---|
nftru | ⊢ Ⅎ𝑥⊤ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1511 | . 2 ⊢ ⊤ | |
2 | 1 | nfth 1764 | 1 ⊢ Ⅎ𝑥⊤ |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1508 Ⅎwnf 1746 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 |
This theorem depends on definitions: df-bi 199 df-tru 1510 df-nf 1747 |
This theorem is referenced by: nfmo 2574 nfeu 2613 moexexvw 2662 2moswapv 2663 2mo 2680 nfceqiOLD 2923 dvelimc 2951 nfral 3168 nfrex 3247 nfreu 3309 nfrmo 3310 nfrab 3319 rabtru 3586 nfsbc 3697 nfcsb 3800 nfdisj 4905 reusv1 5147 reusv2lem1 5148 nfiota 6153 nfriota 6944 nfixp 8276 eqri 30026 esumnul 30980 hasheuni 31017 wl-cbvalnae 34244 wl-equsal 34251 limsup10ex 41510 liminf10ex 41511 liminfvalxr 41520 liminf0 41530 stowei 41805 ioosshoi 42407 vonioolem2 42419 |
Copyright terms: Public domain | W3C validator |