Theorem elmapfn 8448

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

Syntax hints:   → wi 4   ∈ wcel 2112   Fn wfn 6331  (class class class)co 7151   ↑_m cmap 8417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-fv 6344  df-ov 7154  df-oprab 7155  df-mpo 7156  df-1st 7694  df-2nd 7695  df-map 8419

This theorem is referenced by:  mapxpen  8705  fsuppmapnn0fiublem  13400  fsuppmapnn0fiub  13401  fsuppmapnn0fiub0  13403  suppssfz  13404  fsuppmapnn0ub  13405  frlmbas  20513  frlmsslsp  20554  eqmat  21117  matplusgcell  21126  matsubgcell  21127  matvscacell  21129  cramerlem1  21380  tmdgsum  22788  fmptco1f1o  30483  islinds5  31077  ellspds  31078  lbsdiflsp0  31221  matmpo  31267  1smat1  31268  actfunsnf1o  32096  actfunsnrndisj  32097  reprinfz1  32114  unccur  35313  matunitlindflem1  35326  matunitlindflem2  35327  poimirlem4  35334  poimirlem5  35335  poimirlem6  35336  poimirlem7  35337  poimirlem10  35340  poimirlem11  35341  poimirlem12  35342  poimirlem16  35346  poimirlem19  35349  poimirlem29  35359  poimirlem30  35360  poimirlem31  35361  broucube  35364  fsuppind  39777  rfovcnvf1od  41071  dssmapnvod  41087  dssmapntrcls  41197  k0004lem3  41218  unirnmap  42200  unirnmapsn  42206  ssmapsn  42208  dvnprodlem1  42947  dvnprodlem3  42949  rrxsnicc  43301  ioorrnopnlem  43305  ovnsubaddlem1  43568  hoiqssbllem1  43620  iccpartrn  44308  iccpartf  44309  iccpartnel  44316  mndpsuppss  45133  mndpfsupp  45138  dflinc2  45177  lincsum  45196  lincresunit2  45245  2arymaptfo  45426  rrx2pnecoorneor  45487  rrx2linest  45514