![]() |
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 1761, but this proof does not use ax-5 1758.) (Contributed by Mario Carneiro, 6-Oct-2016.) |
Ref | Expression |
---|---|
nftru |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1448 |
. 2
![]() ![]() | |
2 | 1 | nfth 1676 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 |
This theorem depends on definitions: df-bi 189 df-tru 1447 df-nf 1668 |
This theorem is referenced by: nfeu 2315 nfmo 2316 nfceqi 2589 dvelimc 2614 nfral 2774 nfrex 2850 nfreu 2965 nfrmo 2966 nfrab 2972 nfsbc 3289 nfcsb 3381 nfdisj 4385 nfiota 5550 nfriota 6261 nfixp 7541 rabtru 28135 eqri 28147 esumnul 28869 hasheuni 28906 wl-cbvalnae 31866 wl-equsal 31873 dvtanlemOLD 31991 stowei 37926 |
Copyright terms: Public domain | W3C validator |