![]() |
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 5384 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → 𝐹 Fn 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 Fn wfn 5230 ⟶wf 5231 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 |
This theorem depends on definitions: df-bi 117 df-f 5239 |
This theorem is referenced by: offeq 6121 difinfsn 7130 ctssdc 7143 nnnninfeq 7157 nninfdcinf 7200 nninfwlporlemd 7201 nninfwlporlem 7202 seqvalcd 10492 seq3feq2 10503 seq3feq 10505 seqfeq3 10545 ser0f 10549 facnn 10742 fac0 10743 resunimafz0 10846 seq3shft 10882 fisumss 11435 prodf1f 11586 efcvgfsum 11710 ennnfonelemfun 12471 ennnfonelemf1 12472 mhmf1o 12937 resmhm2b 12956 mhmima 12958 mhmeql 12959 grpinvf1o 13029 ghmrn 13213 ghmpreima 13222 ghmeql 13223 ghmnsgima 13224 ghmnsgpreima 13225 ghmeqker 13227 ghmf1o 13231 rhmf1o 13535 psrbaglesuppg 13967 cnrest2 14213 lmss 14223 lmtopcnp 14227 upxp 14249 uptx 14251 cnmpt11 14260 cnmpt21 14268 cnmpt22f 14272 cnmptcom 14275 hmeof1o2 14285 psmetxrge0 14309 isxmet2d 14325 blelrnps 14396 blelrn 14397 xmetresbl 14417 comet 14476 bdxmet 14478 xmettx 14487 dvidlemap 14637 dvaddxxbr 14642 dvmulxxbr 14643 dvrecap 14654 nninfall 15237 nninfsellemeqinf 15244 nninffeq 15248 refeq 15255 |
Copyright terms: Public domain | W3C validator |