Theorem elmapfn 8429

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

Syntax hints:   → wi 4   ∈ wcel 2114   Fn wfn 6350  (class class class)co 7156   ↑_m cmap 8406

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161  df-1st 7689  df-2nd 7690  df-map 8408

This theorem is referenced by:  mapxpen  8683  fsuppmapnn0fiublem  13359  fsuppmapnn0fiub  13360  fsuppmapnn0fiub0  13362  suppssfz  13363  fsuppmapnn0ub  13364  frlmbas  20899  frlmsslsp  20940  eqmat  21033  matplusgcell  21042  matsubgcell  21043  matvscacell  21045  cramerlem1  21296  tmdgsum  22703  fmptco1f1o  30378  islinds5  30932  ellspds  30933  lbsdiflsp0  31022  matmpo  31068  1smat1  31069  actfunsnf1o  31875  actfunsnrndisj  31876  reprinfz1  31893  unccur  34890  matunitlindflem1  34903  matunitlindflem2  34904  poimirlem4  34911  poimirlem5  34912  poimirlem6  34913  poimirlem7  34914  poimirlem10  34917  poimirlem11  34918  poimirlem12  34919  poimirlem16  34923  poimirlem19  34926  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  broucube  34941  rfovcnvf1od  40370  dssmapnvod  40386  dssmapntrcls  40498  k0004lem3  40519  unirnmap  41491  unirnmapsn  41497  ssmapsn  41499  dvnprodlem1  42251  dvnprodlem3  42253  rrxsnicc  42605  ioorrnopnlem  42609  ovnsubaddlem1  42872  hoiqssbllem1  42924  iccpartrn  43610  iccpartf  43611  iccpartnel  43618  mndpsuppss  44439  mndpfsupp  44444  dflinc2  44485  lincsum  44504  lincresunit2  44553  rrx2pnecoorneor  44722  rrx2linest  44749