Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > funeqi | Unicode version |
Description: Equality inference for the function predicate. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
funeqi.1 |
Ref | Expression |
---|---|
funeqi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funeqi.1 | . 2 | |
2 | funeq 5138 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wceq 1331 wfun 5112 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-in 3072 df-ss 3079 df-br 3925 df-opab 3985 df-rel 4541 df-cnv 4542 df-co 4543 df-fun 5120 |
This theorem is referenced by: funmpt 5156 funmpt2 5157 funprg 5168 funtpg 5169 funtp 5171 funcnvuni 5187 f1cnvcnv 5334 f1co 5335 fun11iun 5381 f10 5394 funoprabg 5863 mpofun 5866 ovidig 5881 tposfun 6150 tfri1dALT 6241 tfrcl 6254 rdgfun 6263 frecfun 6285 frecfcllem 6294 th3qcor 6526 ssdomg 6665 sbthlem7 6844 sbthlemi8 6845 casefun 6963 caseinj 6967 djufun 6982 djuinj 6984 ctssdccl 6989 axaddf 7669 axmulf 7670 strleund 12036 strleun 12037 1strbas 12047 2strbasg 12049 2stropg 12050 |
Copyright terms: Public domain | W3C validator |