Theorem elmapfn 8871

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   Fn wfn 6526  (class class class)co 7412   ↑_m cmap 8831

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7990  df-2nd 7991  df-map 8833

This theorem is used by:  mapxpen  9146  fsuppmapnn0fiublem  14113  fsuppmapnn0fiub  14114  fsuppmapnn0fiub0  14116  suppssfz  14117  fsuppmapnn0ub  14118  s3rex  15081  mndpsuppss  18939  mndpfsupp  18941  frlmbas  22041  frlmsslsp  22082  eqmat  22719  matplusgcell  22728  matsubgcell  22729  matvscacell  22731  matunitlindflem1  22974  matunitlindflem2  22975  cramerlem1  22985  tmdgsum  24394  fmptco1f1o  33209  islinds5  33905  ellspds  33906  1arithidomlem2  34050  1arithidom  34051  selvply1rhmlemb  34133  lbsdiflsp0  34240  matmpo  34417  1smat1  34418  actfunsnf1o  35216  actfunsnrndisj  35217  reprinfz1  35234  unccur  38494  poimirlem4  38510  poimirlem5  38511  poimirlem6  38512  poimirlem7  38513  poimirlem10  38516  poimirlem11  38517  poimirlem12  38518  poimirlem16  38522  poimirlem19  38525  poimirlem29  38535  poimirlem30  38536  poimirlem31  38537  broucube  38540  fsuppind  43580  ofoafo  44316  ofoaass  44320  ofoacom  44321  rfovcnvf1od  44963  dssmapnvod  44979  dssmapntrcls  45087  k0004lem3  45108  unirnmap  46164  unirnmapsn  46170  ssmapsn  46172  dvnprodlem1  46900  dvnprodlem3  46902  rrxsnicc  47254  ioorrnopnlem  47258  ovnsubaddlem1  47524  hoiqssbllem1  47576  tmachlem-agreeprod  47891  iccpartrn  48456  iccpartf  48457  iccpartnel  48464  dflinc2  49466  lincsum  49485  lincresunit2  49534  2arymaptfo  49710  rrx2pnecoorneor  49771  rrx2linest  49798  crosspaltd  50910