MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elmapfn Structured version   Unicode version

Theorem elmapfn 7442
Description: A mapping is a function with the appropriate domain. (Contributed by AV, 6-Apr-2019.)
Assertion
Ref Expression
elmapfn  |-  ( A  e.  ( B  ^m  C )  ->  A  Fn  C )

Proof of Theorem elmapfn
StepHypRef Expression
1 elmapi 7441 . 2  |-  ( A  e.  ( B  ^m  C )  ->  A : C --> B )
2 ffn 5682 . 2  |-  ( A : C --> B  ->  A  Fn  C )
31, 2syl 17 1  |-  ( A  e.  ( B  ^m  C )  ->  A  Fn  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1872    Fn wfn 5532   -->wf 5533  (class class class)co 6242    ^m cmap 7420
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402  ax-sep 4482  ax-nul 4491  ax-pow 4538  ax-pr 4596  ax-un 6534
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-ral 2713  df-rex 2714  df-rab 2717  df-v 3018  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3698  df-if 3848  df-pw 3919  df-sn 3935  df-pr 3937  df-op 3941  df-uni 4156  df-iun 4237  df-br 4360  df-opab 4419  df-mpt 4420  df-id 4704  df-xp 4795  df-rel 4796  df-cnv 4797  df-co 4798  df-dm 4799  df-rn 4800  df-res 4801  df-ima 4802  df-iota 5501  df-fun 5539  df-fn 5540  df-f 5541  df-fv 5545  df-ov 6245  df-oprab 6246  df-mpt2 6247  df-1st 6744  df-2nd 6745  df-map 7422
This theorem is referenced by:  mapxpen  7684  fsuppmapnn0fiublem  12145  fsuppmapnn0fiub  12146  fsuppmapnn0fiub0  12148  suppssfz  12149  fsuppmapnn0ub  12150  frlmbas  19253  frlmsslsp  19289  eqmat  19384  matplusgcell  19393  matsubgcell  19394  matvscacell  19396  cramerlem1  19647  tmdgsum  21045  matmpt2  28574  1smat1  28575  poimirlem4  31845  poimirlem5  31846  poimirlem6  31847  poimirlem7  31848  poimirlem10  31851  poimirlem11  31852  poimirlem12  31853  poimirlem16  31857  poimirlem19  31860  poimirlem29  31870  poimirlem30  31871  poimirlem31  31872  broucube  31875  dvnprodlem1  37698  dvnprodlem3  37700  ovnsubaddlem1  38233  iccpartrn  38551  iccpartf  38552  iccpartnel  38559  mndpsuppss  39743  mndpfsupp  39748  dflinc2  39790  lincsum  39809  lincresunit2  39858
  Copyright terms: Public domain W3C validator