Theorem elmapfn 8805

Description: A mapping is a function with the appropriate domain. (Contributed by AV, 6-Apr-2019.)

Assertion

Ref	Expression
elmapfn	⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴 Fn 𝐶)

Proof of Theorem elmapfn

Step	Hyp	Ref	Expression
1		elmapi 8789	. 2 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴:𝐶⟶𝐵)
2	1	ffnd 6663	1 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴 Fn 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2114   Fn wfn 6487  (class class class)co 7360   ↑_m cmap 8766

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-1st 7935  df-2nd 7936  df-map 8768

This theorem is referenced by:  mapxpen  9074  fsuppmapnn0fiublem  13943  fsuppmapnn0fiub  13944  fsuppmapnn0fiub0  13946  suppssfz  13947  fsuppmapnn0ub  13948  mndpsuppss  18724  mndpfsupp  18726  frlmbas  21745  frlmsslsp  21786  eqmat  22399  matplusgcell  22408  matsubgcell  22409  matvscacell  22411  cramerlem1  22662  tmdgsum  24070  fmptco1f1o  32721  islinds5  33442  ellspds  33443  1arithidomlem2  33611  1arithidom  33612  lbsdiflsp0  33786  matmpo  33963  1smat1  33964  actfunsnf1o  34764  actfunsnrndisj  34765  reprinfz1  34782  unccur  37938  matunitlindflem1  37951  matunitlindflem2  37952  poimirlem4  37959  poimirlem5  37960  poimirlem6  37961  poimirlem7  37962  poimirlem10  37965  poimirlem11  37966  poimirlem12  37967  poimirlem16  37971  poimirlem19  37974  poimirlem29  37984  poimirlem30  37985  poimirlem31  37986  broucube  37989  fsuppind  43037  ofoafo  43802  ofoaass  43806  ofoacom  43807  rfovcnvf1od  44449  dssmapnvod  44465  dssmapntrcls  44573  k0004lem3  44594  unirnmap  45655  unirnmapsn  45661  ssmapsn  45663  dvnprodlem1  46392  dvnprodlem3  46394  rrxsnicc  46746  ioorrnopnlem  46750  ovnsubaddlem1  47016  hoiqssbllem1  47068  iccpartrn  47902  iccpartf  47903  iccpartnel  47910  dflinc2  48898  lincsum  48917  lincresunit2  48966  2arymaptfo  49142  rrx2pnecoorneor  49203  rrx2linest  49230