![]() |
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 5248 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-in 3147 df-ss 3154 df-br 4016 df-opab 4077 df-rel 4645 df-cnv 4646 df-co 4647 df-fun 5230 |
This theorem is referenced by: funmpt 5266 funmpt2 5267 funprg 5278 funtpg 5279 funtp 5281 funcnvuni 5297 f1cnvcnv 5444 f1co 5445 fun11iun 5494 f10 5507 funoprabg 5987 mpofun 5990 ovidig 6006 tposfun 6275 tfri1dALT 6366 tfrcl 6379 rdgfun 6388 frecfun 6410 frecfcllem 6419 th3qcor 6653 ssdomg 6792 sbthlem7 6976 sbthlemi8 6977 casefun 7098 caseinj 7102 djufun 7117 djuinj 7119 ctssdccl 7124 axaddf 7881 axmulf 7882 strleund 12577 strleun 12578 1strbas 12591 2strbasg 12593 2stropg 12594 lidlmex 13664 |
Copyright terms: Public domain | W3C validator |