Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > weqi | GIF version |
Description: Type of an equality. |
Ref | Expression |
---|---|
weqi.1 | ⊢ A:α |
weqi.2 | ⊢ B:α |
Ref | Expression |
---|---|
weqi | ⊢ [A = B]:∗ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | weq 38 | . 2 ⊢ = :(α → (α → ∗)) | |
2 | weqi.1 | . 2 ⊢ A:α | |
3 | weqi.2 | . 2 ⊢ B:α | |
4 | 1, 2, 3 | wov 64 | 1 ⊢ [A = B]:∗ |
Colors of variables: type var term |
Syntax hints: ∗hb 3 = ke 7 [kbr 9 wffMMJ2t 12 |
This theorem is referenced by: clf 105 ovl 107 wal 124 wan 126 wim 127 weu 131 alval 132 exval 133 euval 134 notval 135 imval 136 orval 137 anval 138 pm2.21 143 dfan2 144 ecase 153 exlimdv2 156 exlimdv 157 ax4e 158 eta 166 cbvf 167 leqf 169 exlimd 171 ac 184 exmid 186 ax8 198 ax9 199 ax10 200 ax11 201 ax12 202 ax13 203 ax14 204 axext 206 axrep 207 axpow 208 axun 209 |
Copyright terms: Public domain | W3C validator |