| 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 5346 |
. 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 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-ext 2213 |
| This theorem depends on definitions: df-bi 117 df-nf 1509 df-sb 1811 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-in 3206 df-ss 3213 df-br 4089 df-opab 4151 df-rel 4732 df-cnv 4733 df-co 4734 df-fun 5328 |
| This theorem is referenced by: funmpt 5364 funmpt2 5365 fununfun 5373 funprg 5380 funtpg 5381 funtp 5383 funcnvuni 5399 f1cnvcnv 5553 f1co 5554 fun11iun 5604 f10 5618 funopdmsn 5834 funoprabg 6120 mpofun 6123 ovidig 6139 tposfun 6426 tfri1dALT 6517 tfrcl 6530 rdgfun 6539 frecfun 6561 frecfcllem 6570 th3qcor 6808 ssdomg 6952 sbthlem7 7162 sbthlemi8 7163 casefun 7284 caseinj 7288 djufun 7303 djuinj 7305 ctssdccl 7310 axaddf 8088 axmulf 8089 fundm2domnop0 11109 strleund 13187 strleun 13188 1strbas 13201 2strbasg 13204 2stropg 13205 lidlmex 14491 usgredg3 16067 ushgredgedg 16079 ushgredgedgloop 16081 |
| Copyright terms: Public domain | W3C validator |