![]() |
Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > HOLE Home > Th. List > weq | Unicode version |
Description: The equality function has
type ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
weq |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-weq 40 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: type var term |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-weq 40 |
This theorem is referenced by: wtru 43 eqcomx 52 weqi 76 eqcomi 79 mpbi 82 eqid 83 ded 84 ceq12 88 leq 91 beta 92 distrc 93 distrl 94 eqtri 95 oveq123 98 hbov 111 clf 115 ovl 117 alval 142 euval 144 imval 146 anval 148 eta 178 cbvf 179 leqf 181 ax10 213 axrep 220 |
Copyright terms: Public domain | W3C validator |