![]() |
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 1910, but this proof does not use ax-5 1906.) (Contributed by Mario Carneiro, 6-Oct-2016.) |
Ref | Expression |
---|---|
nftru | ⊢ Ⅎ𝑥⊤ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1538 | . 2 ⊢ ⊤ | |
2 | 1 | nfth 1796 | 1 ⊢ Ⅎ𝑥⊤ |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1535 Ⅎwnf 1778 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 |
This theorem depends on definitions: df-bi 206 df-tru 1537 df-nf 1779 |
This theorem is referenced by: nfsb 2518 nfmov 2550 nfmo 2552 nfeuw 2583 nfeu 2584 dvelimc 2928 nfralwOLD 3306 nfrexw 3307 nfral 3367 nfrex 3368 nfreuwOLD 3419 nfrmowOLD 3420 nfrmo 3427 nfreu 3428 nfrabw 3465 nfrabwOLD 3466 nfrab 3469 rabtru 3679 nfsbcw 3798 nfsbc 3801 nfcsbw 3919 nfcsb 3920 eqri 4000 nfdisjw 5125 nfdisj 5126 nfopab 5217 nfiotaw 6504 nfiota 6506 nfriota 7389 nfixpw 8935 nfixp 8936 esumnul 33667 hasheuni 33704 wl-cbvalnae 37000 wl-equsal 37008 limsup10ex 45161 liminf10ex 45162 liminfvalxr 45171 liminf0 45181 stowei 45452 ioosshoi 46057 vonioolem2 46069 |
Copyright terms: Public domain | W3C validator |