Theorem elmapi 8796

Description: A mapping is a function, forward direction only with superfluous antecedent removed. (Contributed by Stefan O'Rear, 10-Oct-2014.)

Assertion

Ref	Expression
elmapi	⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴:𝐶⟶𝐵)

Proof of Theorem elmapi

Step	Hyp	Ref	Expression
1		elmapex 8795	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 8786	. . 3 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐴 ∈ (𝐵 ↑m 𝐶) ↔ 𝐴:𝐶⟶𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐴 ∈ (𝐵 ↑m 𝐶) ↔ 𝐴:𝐶⟶𝐵))
4	3	ibi 267	1 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴:𝐶⟶𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  Vcvv 3429  ⟶wf 6494  (class class class)co 7367   ↑_m cmap 8773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-1st 7942  df-2nd 7943  df-map 8775

This theorem is referenced by:  mapfset  8797  elmapfn  8812  elmapfun  8813  elmapssres  8814  mapsspm  8824  mapfvd  8827  elmapresaun  8828  map0b  8831  mapss  8837  mapsncnv  8841  ralxpmap  8844  mapen  9079  mapxpen  9081  mapunen  9084  mapfienlem1  9318  mapfienlem2  9319  mapfienlem3  9320  mapfien  9321  wemaplem2  9462  wemappo  9464  wemapsolem  9465  wemapso  9466  wemapso2lem  9467  wemapwe  9618  iunmapdisj  9945  fseqenlem1  9946  fseqenlem2  9947  numacn  9971  finacn  9972  acndom  9973  acndom2  9976  infpwfien  9984  infmap2  10139  fin23lem40  10273  isf32lem12  10286  isf34lem6  10302  acncc  10362  pwfseqlem3  10583  pwxpndom2  10588  ramval  16979  ramub  16984  ramcl  17000  prmgaplem7  17028  prmgaplem8  17029  imasdsval2  17480  funcf2  17835  funcpropd  17869  funcestrcsetclem8  18113  funcestrcsetclem9  18114  funcsetcestrclem8  18128  funcsetcestrclem9  18129  mndpsuppss  18733  mndvcl  18765  mndvass  18766  mndvlid  18767  mndvrid  18768  mhmvlin  18769  fsfnn0gsumfsffz  19958  gsummptnn0fzfv  19962  frlmfibas  21742  frlmbas3  21756  frlmipval  21759  frlmphllem  21760  frlmphl  21761  elfilspd  21783  islindf4  21818  psrbagf  21898  mplbas2  22020  ltbwe  22022  evlsvvvallem  22069  evlsvvval  22071  psr1baslem  22148  psr1basf  22165  fvcoe1  22171  coe1mul2lem1  22232  ply1coe  22263  mamures  22362  grpvlinv  22363  grpvrinv  22364  mamucl  22366  mamuass  22367  mamudi  22368  mamudir  22369  mamuvs1  22370  mamuvs2  22371  mamulid  22406  mamurid  22407  mattposcl  22418  mattpostpos  22419  tposmap  22422  mamutpos  22423  matgsumcl  22425  mavmulcl  22512  mavmulass  22514  mavmulsolcl  22516  marepvcl  22534  1marepvmarrepid  22540  mdetleib2  22553  mdetf  22560  mdetdiaglem  22563  mdetrlin  22567  mdetrsca  22568  mdetralt  22573  mdetunilem7  22583  mdetunilem9  22585  maducoeval2  22605  madutpos  22607  madugsum  22608  madurid  22609  cramerimplem1  22648  m2pmfzmap  22712  decpmatval  22730  pmatcollpw3lem  22748  pmatcollpw3fi1lem1  22751  pmatcollpw3fi1lem2  22752  pm2mp  22790  chfacfisf  22819  chfacfisfcpmat  22820  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  chfacfpmmulgsum2  22830  cayhamlem1  22831  cpmadugsumlemF  22841  cpmadugsumfi  22842  cayhamlem2  22849  chcoeffeqlem  22850  cayleyhamilton1  22857  pnrmopn  23308  xkoptsub  23619  xkopt  23620  tmdgsum  24060  imasdsf1olem  24338  rrxnm  25358  rrxds  25360  rrxf  25368  rrxmvallem  25371  rrxbasefi  25377  rrxdsfi  25378  ehlbase  25382  ovolscalem2  25481  uniioombl  25556  tdeglem2  26026  plypf1  26177  ulmclm  26352  ulmcaulem  26359  ulmcau  26360  ulmss  26362  ulmbdd  26363  ulmcn  26364  ulmdvlem1  26365  ulmdvlem2  26366  ulmdvlem3  26367  mtest  26369  mtestbdd  26370  mbfulm  26371  iblulm  26372  itgulm  26373  itgulm2  26374  adjval2  31962  fmptco1f1o  32706  fcobijfs  32794  fcobijfs2  32795  resf1o  32803  fpwrelmap  32806  elrspunidl  33488  elrspunsn  33489  1arithidomlem2  33596  1arithidom  33597  fply1  33618  psrbasfsupp  33672  ply1degltdimlem  33766  fedgmullem1  33773  fedgmul  33775  extdg1id  33810  smatrcl  33940  mbfmf  34398  elmbfmvol2  34411  eulerpartlemelr  34501  eulerpartlemf  34514  eulerpartlemt  34515  eulerpartgbij  34516  eulerpartlemgu  34521  eulerpartlemgh  34522  eulerpartlemgf  34523  eulerpartlemgs2  34524  reprf  34756  reprsuc  34759  vtsprod  34783  circlemethhgt  34787  tgoldbachgtd  34806  satfv1lem  35544  satfvel  35594  satefvfmla0  35600  satefvfmla1  35607  prv1n  35613  mrsubff1  35696  mrsub0  35698  mrsubf  35699  mrsubccat  35700  mrsubcn  35701  msubrn  35711  msubff  35712  msubf  35714  msubff1  35738  mclsind  35752  uncf  37920  curunc  37923  unccur  37924  matunitlindflem1  37937  matunitlindflem2  37938  poimirlem4  37945  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  poimir  37974  broucube  37975  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  rrnmet  38150  rrndstprj1  38151  rrndstprj2  38152  rrncmslem  38153  rrnequiv  38156  aks6d1c2lem4  42566  mapcod  42682  evlselv  43020  fsuppind  43023  mhphf  43030  mapco2g  43146  mapfzcons1  43149  mapfzcons2  43151  mzpcompact2lem  43183  eldiophb  43189  elmapresaunres2  43203  eq0rabdioph  43208  rexrabdioph  43222  eldioph4b  43239  diophren  43241  rmydioph  43442  rmxdioph  43444  expdiophlem2  43450  expdioph  43451  pw2f1o2val2  43468  wepwsolem  43470  pwfi2f1o  43524  ofoafo  43784  ofoaid1  43786  ofoaid2  43787  ofoaass  43788  ofoacom  43789  rfovcnvf1od  44431  rfovcnvfvd  44434  fsovrfovd  44436  fsovcnvlem  44440  ntrk0kbimka  44466  neik0pk1imk0  44474  ntrclsfveq1  44487  ntrclsfveq2  44488  ntrclsfveq  44489  ntrclsss  44490  ntrclsiso  44494  ntrclsk2  44495  ntrclskb  44496  ntrclsk3  44497  ntrclsk13  44498  ntrclsk4  44499  ntrneifv3  44509  ntrneineine0lem  44510  ntrneineine1lem  44511  ntrneifv4  44512  ntrneiel2  44513  ntrneicls00  44516  ntrneicls11  44517  ntrneiiso  44518  ntrneik2  44519  ntrneikb  44521  ntrneixb  44522  ntrneik3  44523  ntrneix3  44524  ntrneik13  44525  ntrneix13  44526  ntrneik4w  44527  ntrneik4  44528  clsneifv3  44537  clsneifv4  44538  neicvgfv  44548  k0004ss2  44579  k0004val0  44581  mnringbasefd  44645  mnugrud  44711  mapss2  45634  difmap  45636  inmap  45638  difmapsn  45641  ssmapsn  45645  mccllem  46027  dvnprodlem1  46374  dvnprodlem2  46375  fourierdlem11  46546  fourierdlem12  46547  fourierdlem13  46548  fourierdlem14  46549  fourierdlem34  46569  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  fourierdlem54  46588  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem69  46603  fourierdlem72  46606  fourierdlem74  46608  fourierdlem75  46609  fourierdlem79  46613  fourierdlem85  46619  fourierdlem88  46622  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem92  46626  fourierdlem94  46628  fourierdlem97  46631  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem113  46647  etransclem24  46686  etransclem26  46688  etransclem27  46689  etransclem28  46690  etransclem31  46693  etransclem32  46694  etransclem33  46695  etransclem34  46696  etransclem35  46697  etransclem37  46699  etransclem38  46700  rrxtopnfi  46715  rrndistlt  46718  qndenserrnbllem  46722  rrxsnicc  46728  ioorrnopnlem  46732  subsaliuncl  46786  hoicvr  46976  ovnprodcl  46982  ovnsupge0  46985  ovnlecvr  46986  ovncvrrp  46992  ovn0lem  46993  ovnsubaddlem1  46998  sge0hsphoire  47017  hoidmv1le  47022  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  hoidmvlelem5  47027  hoidmvle  47028  ovnhoilem2  47030  ovnlecvr2  47038  ovncvr2  47039  hoiqssbllem1  47050  hoiqssbllem2  47051  hoiqssbllem3  47052  hspmbllem2  47055  opnvonmbllem2  47061  ovolval2lem  47071  ovolval2  47072  ovolval3  47075  ovolval4lem2  47078  ovolval5lem3  47082  ovnovollem1  47084  ovnovollem2  47085  vonvolmbllem  47088  vonvolmbl2  47091  vonvol2  47092  snvonmbl  47114  vonsn  47119  iccpartxr  47879  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  intop  48679  assintop  48685  isassintop  48686  ofaddmndmap  48819  rmsupp0  48844  domnmsuppn0  48845  rmsuppss  48846  scmsuppss  48847  gsumlsscl  48856  lincfsuppcl  48889  linccl  48890  lcosn0  48896  lincdifsn  48900  lincsum  48905  lincscm  48906  lincscmcl  48908  islinindfis  48925  lincext1  48930  lincext2  48931  lincext3  48932  lindslinindimp2lem1  48934  lindslinindimp2lem2  48935  lindslinindimp2lem4  48937  lindslinindsimp2lem5  48938  snlindsntor  48947  lincresunitlem2  48952  lincresunit3lem1  48955  lincresunit3lem2  48956  lincresunit3  48957  lincreslvec3  48958  isldepslvec2  48961  zlmodzxzldeplem2  48977  zlmodzxzldeplem3  48978  ldepsnlinclem1  48981  ldepsnlinclem2  48982  1arymaptf1  49118  1arymaptfo  49119  2arympt  49125  2arymaptf1  49129  2arymaptfo  49130  prelrrx2b  49190  eenglngeehlnmlem1  49213  eenglngeehlnmlem2  49214  aacllem  50276