Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ffnd | Unicode version |
Description: A mapping is a function with domain, deduction form. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Ref | Expression |
---|---|
ffnd.1 |
Ref | Expression |
---|---|
ffnd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffnd.1 | . 2 | |
2 | ffn 5242 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wfn 5088 wf 5089 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-f 5097 |
This theorem is referenced by: offeq 5963 difinfsn 6953 ctssdc 6966 seqvalcd 10200 seq3feq2 10211 seq3feq 10213 seqfeq3 10253 ser0f 10256 facnn 10441 fac0 10442 resunimafz0 10542 seq3shft 10578 fisumss 11129 efcvgfsum 11300 ennnfonelemfun 11857 ennnfonelemf1 11858 cnrest2 12332 lmss 12342 lmtopcnp 12346 upxp 12368 uptx 12370 cnmpt11 12379 cnmpt21 12387 cnmpt22f 12391 cnmptcom 12394 hmeof1o2 12404 psmetxrge0 12428 isxmet2d 12444 blelrnps 12515 blelrn 12516 xmetresbl 12536 comet 12595 bdxmet 12597 xmettx 12606 dvidlemap 12756 dvaddxxbr 12761 dvmulxxbr 12762 dvrecap 12773 nninfalllemn 13129 nninfall 13131 nninfsellemeqinf 13139 nninffeq 13143 refeq 13150 |
Copyright terms: Public domain | W3C validator |