Theorem elmapi 8646

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 8645	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 8637	. . 3 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐴 ∈ (𝐵 ↑m 𝐶) ↔ 𝐴:𝐶⟶𝐵))
3	1, 2	syl 17	. 2 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐴 ∈ (𝐵 ↑m 𝐶) ↔ 𝐴:𝐶⟶𝐵))
4	3	ibi 266	1 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → 𝐴:𝐶⟶𝐵)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2107  Vcvv 3433  ⟶wf 6433  (class class class)co 7284   ↑_m cmap 8624

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289  df-1st 7840  df-2nd 7841  df-map 8626

This theorem is referenced by:  mapfset  8647  elmapfn  8662  elmapfun  8663  elmapssres  8664  mapsspm  8673  mapfvd  8676  elmapresaun  8677  map0b  8680  mapss  8686  mapsncnv  8690  ralxpmap  8693  mapen  8937  mapxpen  8939  mapunen  8942  mapfienlem1  9173  mapfienlem2  9174  mapfienlem3  9175  mapfien  9176  wemaplem2  9315  wemappo  9317  wemapsolem  9318  wemapso  9319  wemapso2lem  9320  wemapwe  9464  iunmapdisj  9788  fseqenlem1  9789  fseqenlem2  9790  numacn  9814  finacn  9815  acndom  9816  acndom2  9819  infpwfien  9827  infmap2  9983  fin23lem40  10116  isf32lem12  10129  isf34lem6  10145  acncc  10205  pwfseqlem3  10425  pwxpndom2  10430  ramval  16718  ramub  16723  ramcl  16739  prmgaplem7  16767  prmgaplem8  16768  imasdsval2  17236  funcf2  17592  funcpropd  17625  funcestrcsetclem8  17873  funcestrcsetclem9  17874  funcsetcestrclem8  17888  funcsetcestrclem9  17889  fsfnn0gsumfsffz  19593  gsummptnn0fzfv  19597  frlmfibas  20978  frlmbas3  20992  frlmipval  20995  frlmphllem  20996  frlmphl  20997  elfilspd  21019  islindf4  21054  psrbagf  21130  mplbas2  21252  ltbwe  21254  psr1baslem  21365  psr1basf  21381  fvcoe1  21387  coe1mul2lem1  21447  ply1coe  21476  mamures  21548  mndvcl  21549  mndvass  21550  mndvlid  21551  mndvrid  21552  grpvlinv  21553  grpvrinv  21554  mhmvlin  21555  mamucl  21557  mamuass  21558  mamudi  21559  mamudir  21560  mamuvs1  21561  mamuvs2  21562  mamulid  21599  mamurid  21600  mattposcl  21611  mattpostpos  21612  tposmap  21615  mamutpos  21616  matgsumcl  21618  mavmulcl  21705  mavmulass  21707  mavmulsolcl  21709  marepvcl  21727  1marepvmarrepid  21733  mdetleib2  21746  mdetf  21753  mdetdiaglem  21756  mdetrlin  21760  mdetrsca  21761  mdetralt  21766  mdetunilem7  21776  mdetunilem9  21778  maducoeval2  21798  madutpos  21800  madugsum  21801  madurid  21802  cramerimplem1  21841  m2pmfzmap  21905  decpmatval  21923  pmatcollpw3lem  21941  pmatcollpw3fi1lem1  21944  pmatcollpw3fi1lem2  21945  pm2mp  21983  chfacfisf  22012  chfacfisfcpmat  22013  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  chfacfpmmulgsum2  22023  cayhamlem1  22024  cpmadugsumlemF  22034  cpmadugsumfi  22035  cayhamlem2  22042  chcoeffeqlem  22043  cayleyhamilton1  22050  pnrmopn  22503  xkoptsub  22814  xkopt  22815  tmdgsum  23255  imasdsf1olem  23535  rrxnm  24564  rrxds  24566  rrxf  24574  rrxmvallem  24577  rrxbasefi  24583  rrxdsfi  24584  ehlbase  24588  ovolscalem2  24687  uniioombl  24762  tdeglem2  25235  plypf1  25382  ulmclm  25555  ulmcaulem  25562  ulmcau  25563  ulmss  25565  ulmbdd  25566  ulmcn  25567  ulmdvlem1  25568  ulmdvlem2  25569  ulmdvlem3  25570  mtest  25572  mtestbdd  25573  mbfulm  25574  iblulm  25575  itgulm  25576  itgulm2  25577  adjval2  30262  fmptco1f1o  30977  fcobijfs  31067  resf1o  31074  fpwrelmap  31077  elrspunidl  31615  fply1  31676  fedgmullem1  31719  fedgmul  31721  extdg1id  31747  smatrcl  31755  mbfmf  32231  elmbfmvol2  32243  eulerpartlemelr  32333  eulerpartlemf  32346  eulerpartlemt  32347  eulerpartgbij  32348  eulerpartlemgu  32353  eulerpartlemgh  32354  eulerpartlemgf  32355  eulerpartlemgs2  32356  reprf  32601  reprsuc  32604  vtsprod  32628  circlemethhgt  32632  tgoldbachgtd  32651  satfv1lem  33333  satfvel  33383  satefvfmla0  33389  satefvfmla1  33396  prv1n  33402  mrsubff1  33485  mrsub0  33487  mrsubf  33488  mrsubccat  33489  mrsubcn  33490  msubrn  33500  msubff  33501  msubf  33503  msubff1  33527  mclsind  33541  uncf  35765  curunc  35768  unccur  35769  matunitlindflem1  35782  matunitlindflem2  35783  poimirlem4  35790  poimirlem5  35791  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem16  35802  poimirlem17  35803  poimirlem18  35804  poimirlem19  35805  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  poimir  35819  broucube  35820  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  rrnmet  35996  rrndstprj1  35997  rrndstprj2  35998  rrncmslem  35999  rrnequiv  36002  evlsbagval  40282  fsuppind  40286  mhphf  40292  mapco2g  40543  mapfzcons1  40546  mapfzcons2  40548  mzpcompact2lem  40580  eldiophb  40586  elmapresaunres2  40600  eq0rabdioph  40605  rexrabdioph  40623  eldioph4b  40640  diophren  40642  rmydioph  40843  rmxdioph  40845  expdiophlem2  40851  expdioph  40852  pw2f1o2val2  40869  wepwsolem  40874  pwfi2f1o  40928  rfovcnvf1od  41619  rfovcnvfvd  41622  fsovrfovd  41624  fsovcnvlem  41628  ntrk0kbimka  41656  neik0pk1imk0  41664  ntrclsfveq1  41677  ntrclsfveq2  41678  ntrclsfveq  41679  ntrclsss  41680  ntrclsiso  41684  ntrclsk2  41685  ntrclskb  41686  ntrclsk3  41687  ntrclsk13  41688  ntrclsk4  41689  ntrneifv3  41699  ntrneineine0lem  41700  ntrneineine1lem  41701  ntrneifv4  41702  ntrneiel2  41703  ntrneicls00  41706  ntrneicls11  41707  ntrneiiso  41708  ntrneik2  41709  ntrneikb  41711  ntrneixb  41712  ntrneik3  41713  ntrneix3  41714  ntrneik13  41715  ntrneix13  41716  ntrneik4w  41717  ntrneik4  41718  clsneifv3  41727  clsneifv4  41728  neicvgfv  41738  k0004ss2  41769  k0004val0  41771  mnringbasefd  41840  mnugrud  41909  mapss2  42752  difmap  42754  inmap  42756  difmapsn  42759  ssmapsn  42763  mccllem  43145  dvnprodlem1  43494  dvnprodlem2  43495  fourierdlem11  43666  fourierdlem12  43667  fourierdlem13  43668  fourierdlem14  43669  fourierdlem34  43689  fourierdlem41  43696  fourierdlem48  43702  fourierdlem49  43703  fourierdlem54  43708  fourierdlem63  43717  fourierdlem64  43718  fourierdlem65  43719  fourierdlem69  43723  fourierdlem72  43726  fourierdlem74  43728  fourierdlem75  43729  fourierdlem79  43733  fourierdlem85  43739  fourierdlem88  43742  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem92  43746  fourierdlem94  43748  fourierdlem97  43751  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  fourierdlem113  43767  etransclem24  43806  etransclem26  43808  etransclem27  43809  etransclem28  43810  etransclem31  43813  etransclem32  43814  etransclem33  43815  etransclem34  43816  etransclem35  43817  etransclem37  43819  etransclem38  43820  rrxtopnfi  43835  rrndistlt  43838  qndenserrnbllem  43842  rrxsnicc  43848  ioorrnopnlem  43852  subsaliuncl  43904  hoicvr  44093  ovnprodcl  44099  ovnsupge0  44102  ovnlecvr  44103  ovncvrrp  44109  ovn0lem  44110  ovnsubaddlem1  44115  sge0hsphoire  44134  hoidmv1le  44139  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvlelem4  44143  hoidmvlelem5  44144  hoidmvle  44145  ovnhoilem2  44147  ovnlecvr2  44155  ovncvr2  44156  hoiqssbllem1  44167  hoiqssbllem2  44168  hoiqssbllem3  44169  hspmbllem2  44172  opnvonmbllem2  44178  ovolval2lem  44188  ovolval2  44189  ovolval3  44192  ovolval4lem2  44195  ovolval5lem3  44199  ovnovollem1  44201  ovnovollem2  44202  vonvolmbllem  44205  vonvolmbl2  44208  vonvol2  44209  snvonmbl  44231  vonsn  44236  iccpartxr  44882  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  intop  45408  assintop  45414  isassintop  45415  ofaddmndmap  45690  rmsupp0  45715  domnmsuppn0  45716  rmsuppss  45717  mndpsuppss  45718  scmsuppss  45719  gsumlsscl  45730  lincfsuppcl  45765  linccl  45766  lcosn0  45772  lincdifsn  45776  lincsum  45781  lincscm  45782  lincscmcl  45784  islinindfis  45801  lincext1  45806  lincext2  45807  lincext3  45808  lindslinindimp2lem1  45810  lindslinindimp2lem2  45811  lindslinindimp2lem4  45813  lindslinindsimp2lem5  45814  snlindsntor  45823  lincresunitlem2  45828  lincresunit3lem1  45831  lincresunit3lem2  45832  lincresunit3  45833  lincreslvec3  45834  isldepslvec2  45837  zlmodzxzldeplem2  45853  zlmodzxzldeplem3  45854  ldepsnlinclem1  45857  ldepsnlinclem2  45858  1arymaptf1  45999  1arymaptfo  46000  2arympt  46006  2arymaptf1  46010  2arymaptfo  46011  prelrrx2b  46071  eenglngeehlnmlem1  46094  eenglngeehlnmlem2  46095  aacllem  46516