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 5331 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wfn 5177 wf 5178 |
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 5186 |
This theorem is referenced by: offeq 6057 difinfsn 7056 ctssdc 7069 nnnninfeq 7083 seqvalcd 10384 seq3feq2 10395 seq3feq 10397 seqfeq3 10437 ser0f 10440 facnn 10629 fac0 10630 resunimafz0 10730 seq3shft 10766 fisumss 11319 prodf1f 11470 efcvgfsum 11594 ennnfonelemfun 12293 ennnfonelemf1 12294 cnrest2 12783 lmss 12793 lmtopcnp 12797 upxp 12819 uptx 12821 cnmpt11 12830 cnmpt21 12838 cnmpt22f 12842 cnmptcom 12845 hmeof1o2 12855 psmetxrge0 12879 isxmet2d 12895 blelrnps 12966 blelrn 12967 xmetresbl 12987 comet 13046 bdxmet 13048 xmettx 13057 dvidlemap 13207 dvaddxxbr 13212 dvmulxxbr 13213 dvrecap 13224 nninfall 13730 nninfsellemeqinf 13737 nninffeq 13741 refeq 13748 |
Copyright terms: Public domain | W3C validator |