Theorem elmapfn 8809

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 8793	. 2 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴:𝐶⟶𝐵)
2	1	ffnd 6663	1 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴 Fn 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2119   Fn wfn 6487  (class class class)co 7363   ↑_m cmap 8770

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-1st 7938  df-2nd 7939  df-map 8772

This theorem is referenced by:  mapxpen  9078  fsuppmapnn0fiublem  13950  fsuppmapnn0fiub  13951  fsuppmapnn0fiub0  13953  suppssfz  13954  fsuppmapnn0ub  13955  mndpsuppss  18731  mndpfsupp  18733  frlmbas  21737  frlmsslsp  21778  eqmat  22414  matplusgcell  22423  matsubgcell  22424  matvscacell  22426  cramerlem1  22677  tmdgsum  24085  fmptco1f1o  32732  islinds5  33457  ellspds  33458  1arithidomlem2  33626  1arithidom  33627  selvply1rhmlemb  33710  lbsdiflsp0  33817  matmpo  33994  1smat1  33995  actfunsnf1o  34795  actfunsnrndisj  34796  reprinfz1  34813  unccur  37977  matunitlindflem1  37990  matunitlindflem2  37991  poimirlem4  37998  poimirlem5  37999  poimirlem6  38000  poimirlem7  38001  poimirlem10  38004  poimirlem11  38005  poimirlem12  38006  poimirlem16  38010  poimirlem19  38013  poimirlem29  38023  poimirlem30  38024  poimirlem31  38025  broucube  38028  fsuppind  43047  ofoafo  43808  ofoaass  43812  ofoacom  43813  rfovcnvf1od  44455  dssmapnvod  44471  dssmapntrcls  44579  k0004lem3  44600  unirnmap  45660  unirnmapsn  45666  ssmapsn  45668  dvnprodlem1  46396  dvnprodlem3  46398  rrxsnicc  46750  ioorrnopnlem  46754  ovnsubaddlem1  47020  hoiqssbllem1  47072  iccpartrn  47912  iccpartf  47913  iccpartnel  47920  dflinc2  48908  lincsum  48927  lincresunit2  48976  2arymaptfo  49152  rrx2pnecoorneor  49213  rrx2linest  49240