Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nftru | Structured version Visualization version Unicode version |
Description: The true constant has no free variables. (This can also be proven in one step with nfv 1843, but this proof does not use ax-5 1839.) (Contributed by Mario Carneiro, 6-Oct-2016.) |
Ref | Expression |
---|---|
nftru |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1487 | . 2 | |
2 | 1 | nfth 1727 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wtru 1484 wnf 1708 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 |
This theorem depends on definitions: df-bi 197 df-tru 1486 df-nf 1710 |
This theorem is referenced by: nfeu 2486 nfmo 2487 nfceqi 2761 dvelimc 2787 nfral 2945 nfrex 3007 nfreu 3114 nfrmo 3115 nfrab 3123 rabtru 3361 nfsbc 3457 nfcsb 3551 nfdisj 4632 nfiota 5855 nfriota 6620 nfixp 7927 eqri 29315 esumnul 30110 hasheuni 30147 wl-cbvalnae 33320 wl-equsal 33326 limsup10ex 40005 liminf10ex 40006 liminfvalxr 40015 liminf0 40025 stowei 40281 ioosshoi 40883 vonioolem2 40895 |
Copyright terms: Public domain | W3C validator |