Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ffnd | GIF 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 | ⊢ (𝜑 → 𝐹 Fn 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffnd.1 | . 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | |
2 | ffn 5272 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → 𝐹 Fn 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 Fn wfn 5118 ⟶wf 5119 |
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 5127 |
This theorem is referenced by: offeq 5995 difinfsn 6985 ctssdc 6998 seqvalcd 10235 seq3feq2 10246 seq3feq 10248 seqfeq3 10288 ser0f 10291 facnn 10476 fac0 10477 resunimafz0 10577 seq3shft 10613 fisumss 11164 prodf1f 11315 efcvgfsum 11376 ennnfonelemfun 11933 ennnfonelemf1 11934 cnrest2 12408 lmss 12418 lmtopcnp 12422 upxp 12444 uptx 12446 cnmpt11 12455 cnmpt21 12463 cnmpt22f 12467 cnmptcom 12470 hmeof1o2 12480 psmetxrge0 12504 isxmet2d 12520 blelrnps 12591 blelrn 12592 xmetresbl 12612 comet 12671 bdxmet 12673 xmettx 12682 dvidlemap 12832 dvaddxxbr 12837 dvmulxxbr 12838 dvrecap 12849 nninfalllemn 13205 nninfall 13207 nninfsellemeqinf 13215 nninffeq 13219 refeq 13226 |
Copyright terms: Public domain | W3C validator |