| 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 5341 |
. 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 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-ext 2211 |
| This theorem depends on definitions: df-bi 117 df-nf 1507 df-sb 1809 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-in 3203 df-ss 3210 df-br 4084 df-opab 4146 df-rel 4727 df-cnv 4728 df-co 4729 df-fun 5323 |
| This theorem is referenced by: funmpt 5359 funmpt2 5360 fununfun 5367 funprg 5374 funtpg 5375 funtp 5377 funcnvuni 5393 f1cnvcnv 5547 f1co 5548 fun11iun 5598 f10 5611 funopdmsn 5826 funoprabg 6112 mpofun 6115 ovidig 6131 tposfun 6417 tfri1dALT 6508 tfrcl 6521 rdgfun 6530 frecfun 6552 frecfcllem 6561 th3qcor 6799 ssdomg 6943 sbthlem7 7146 sbthlemi8 7147 casefun 7268 caseinj 7272 djufun 7287 djuinj 7289 ctssdccl 7294 axaddf 8071 axmulf 8072 fundm2domnop0 11085 strleund 13157 strleun 13158 1strbas 13171 2strbasg 13174 2stropg 13175 lidlmex 14460 usgredg3 16033 ushgredgedg 16045 ushgredgedgloop 16047 |
| Copyright terms: Public domain | W3C validator |