Theorem elmapi 8825

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 8824	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 8815	. . 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 2109  Vcvv 3450  ⟶wf 6510  (class class class)co 7390   ↑_m cmap 8802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-1st 7971  df-2nd 7972  df-map 8804

This theorem is referenced by:  mapfset  8826  elmapfn  8841  elmapfun  8842  elmapssres  8843  mapsspm  8852  mapfvd  8855  elmapresaun  8856  map0b  8859  mapss  8865  mapsncnv  8869  ralxpmap  8872  mapen  9111  mapxpen  9113  mapunen  9116  mapfienlem1  9363  mapfienlem2  9364  mapfienlem3  9365  mapfien  9366  wemaplem2  9507  wemappo  9509  wemapsolem  9510  wemapso  9511  wemapso2lem  9512  wemapwe  9657  iunmapdisj  9983  fseqenlem1  9984  fseqenlem2  9985  numacn  10009  finacn  10010  acndom  10011  acndom2  10014  infpwfien  10022  infmap2  10177  fin23lem40  10311  isf32lem12  10324  isf34lem6  10340  acncc  10400  pwfseqlem3  10620  pwxpndom2  10625  ramval  16986  ramub  16991  ramcl  17007  prmgaplem7  17035  prmgaplem8  17036  imasdsval2  17486  funcf2  17837  funcpropd  17871  funcestrcsetclem8  18115  funcestrcsetclem9  18116  funcsetcestrclem8  18130  funcsetcestrclem9  18131  mndpsuppss  18699  mndvcl  18731  mndvass  18732  mndvlid  18733  mndvrid  18734  mhmvlin  18735  fsfnn0gsumfsffz  19920  gsummptnn0fzfv  19924  frlmfibas  21678  frlmbas3  21692  frlmipval  21695  frlmphllem  21696  frlmphl  21697  elfilspd  21719  islindf4  21754  psrbagf  21834  mplbas2  21956  ltbwe  21958  psr1baslem  22076  psr1basf  22093  fvcoe1  22099  coe1mul2lem1  22160  ply1coe  22192  mamures  22291  grpvlinv  22292  grpvrinv  22293  mamucl  22295  mamuass  22296  mamudi  22297  mamudir  22298  mamuvs1  22299  mamuvs2  22300  mamulid  22335  mamurid  22336  mattposcl  22347  mattpostpos  22348  tposmap  22351  mamutpos  22352  matgsumcl  22354  mavmulcl  22441  mavmulass  22443  mavmulsolcl  22445  marepvcl  22463  1marepvmarrepid  22469  mdetleib2  22482  mdetf  22489  mdetdiaglem  22492  mdetrlin  22496  mdetrsca  22497  mdetralt  22502  mdetunilem7  22512  mdetunilem9  22514  maducoeval2  22534  madutpos  22536  madugsum  22537  madurid  22538  cramerimplem1  22577  m2pmfzmap  22641  decpmatval  22659  pmatcollpw3lem  22677  pmatcollpw3fi1lem1  22680  pmatcollpw3fi1lem2  22681  pm2mp  22719  chfacfisf  22748  chfacfisfcpmat  22749  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  chfacfpmmulgsum2  22759  cayhamlem1  22760  cpmadugsumlemF  22770  cpmadugsumfi  22771  cayhamlem2  22778  chcoeffeqlem  22779  cayleyhamilton1  22786  pnrmopn  23237  xkoptsub  23548  xkopt  23549  tmdgsum  23989  imasdsf1olem  24268  rrxnm  25298  rrxds  25300  rrxf  25308  rrxmvallem  25311  rrxbasefi  25317  rrxdsfi  25318  ehlbase  25322  ovolscalem2  25422  uniioombl  25497  tdeglem2  25973  plypf1  26124  ulmclm  26303  ulmcaulem  26310  ulmcau  26311  ulmss  26313  ulmbdd  26314  ulmcn  26315  ulmdvlem1  26316  ulmdvlem2  26317  ulmdvlem3  26318  mtest  26320  mtestbdd  26321  mbfulm  26322  iblulm  26323  itgulm  26324  itgulm2  26325  adjval2  31827  fmptco1f1o  32564  fcobijfs  32653  resf1o  32660  fpwrelmap  32663  elrspunidl  33406  elrspunsn  33407  1arithidomlem2  33514  1arithidom  33515  fply1  33534  ply1degltdimlem  33625  fedgmullem1  33632  fedgmul  33634  extdg1id  33668  smatrcl  33793  mbfmf  34251  elmbfmvol2  34265  eulerpartlemelr  34355  eulerpartlemf  34368  eulerpartlemt  34369  eulerpartgbij  34370  eulerpartlemgu  34375  eulerpartlemgh  34376  eulerpartlemgf  34377  eulerpartlemgs2  34378  reprf  34610  reprsuc  34613  vtsprod  34637  circlemethhgt  34641  tgoldbachgtd  34660  satfv1lem  35356  satfvel  35406  satefvfmla0  35412  satefvfmla1  35419  prv1n  35425  mrsubff1  35508  mrsub0  35510  mrsubf  35511  mrsubccat  35512  mrsubcn  35513  msubrn  35523  msubff  35524  msubf  35526  msubff1  35550  mclsind  35564  uncf  37600  curunc  37603  unccur  37604  matunitlindflem1  37617  matunitlindflem2  37618  poimirlem4  37625  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  poimir  37654  broucube  37655  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  rrnmet  37830  rrndstprj1  37831  rrndstprj2  37832  rrncmslem  37833  rrnequiv  37836  aks6d1c2lem4  42122  mapcod  42238  evlsvvvallem  42556  evlsvvval  42558  evlselv  42582  fsuppind  42585  mhphf  42592  mapco2g  42709  mapfzcons1  42712  mapfzcons2  42714  mzpcompact2lem  42746  eldiophb  42752  elmapresaunres2  42766  eq0rabdioph  42771  rexrabdioph  42789  eldioph4b  42806  diophren  42808  rmydioph  43010  rmxdioph  43012  expdiophlem2  43018  expdioph  43019  pw2f1o2val2  43036  wepwsolem  43038  pwfi2f1o  43092  ofoafo  43352  ofoaid1  43354  ofoaid2  43355  ofoaass  43356  ofoacom  43357  rfovcnvf1od  44000  rfovcnvfvd  44003  fsovrfovd  44005  fsovcnvlem  44009  ntrk0kbimka  44035  neik0pk1imk0  44043  ntrclsfveq1  44056  ntrclsfveq2  44057  ntrclsfveq  44058  ntrclsss  44059  ntrclsiso  44063  ntrclsk2  44064  ntrclskb  44065  ntrclsk3  44066  ntrclsk13  44067  ntrclsk4  44068  ntrneifv3  44078  ntrneineine0lem  44079  ntrneineine1lem  44080  ntrneifv4  44081  ntrneiel2  44082  ntrneicls00  44085  ntrneicls11  44086  ntrneiiso  44087  ntrneik2  44088  ntrneikb  44090  ntrneixb  44091  ntrneik3  44092  ntrneix3  44093  ntrneik13  44094  ntrneix13  44095  ntrneik4w  44096  ntrneik4  44097  clsneifv3  44106  clsneifv4  44107  neicvgfv  44117  k0004ss2  44148  k0004val0  44150  mnringbasefd  44214  mnugrud  44280  mapss2  45206  difmap  45208  inmap  45210  difmapsn  45213  ssmapsn  45217  mccllem  45602  dvnprodlem1  45951  dvnprodlem2  45952  fourierdlem11  46123  fourierdlem12  46124  fourierdlem13  46125  fourierdlem14  46126  fourierdlem34  46146  fourierdlem41  46153  fourierdlem48  46159  fourierdlem49  46160  fourierdlem54  46165  fourierdlem63  46174  fourierdlem64  46175  fourierdlem65  46176  fourierdlem69  46180  fourierdlem72  46183  fourierdlem74  46185  fourierdlem75  46186  fourierdlem79  46190  fourierdlem85  46196  fourierdlem88  46199  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem92  46203  fourierdlem94  46205  fourierdlem97  46208  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem113  46224  etransclem24  46263  etransclem26  46265  etransclem27  46266  etransclem28  46267  etransclem31  46270  etransclem32  46271  etransclem33  46272  etransclem34  46273  etransclem35  46274  etransclem37  46276  etransclem38  46277  rrxtopnfi  46292  rrndistlt  46295  qndenserrnbllem  46299  rrxsnicc  46305  ioorrnopnlem  46309  subsaliuncl  46363  hoicvr  46553  ovnprodcl  46559  ovnsupge0  46562  ovnlecvr  46563  ovncvrrp  46569  ovn0lem  46570  ovnsubaddlem1  46575  sge0hsphoire  46594  hoidmv1le  46599  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  hoidmvlelem5  46604  hoidmvle  46605  ovnhoilem2  46607  ovnlecvr2  46615  ovncvr2  46616  hoiqssbllem1  46627  hoiqssbllem2  46628  hoiqssbllem3  46629  hspmbllem2  46632  opnvonmbllem2  46638  ovolval2lem  46648  ovolval2  46649  ovolval3  46652  ovolval4lem2  46655  ovolval5lem3  46659  ovnovollem1  46661  ovnovollem2  46662  vonvolmbllem  46665  vonvolmbl2  46668  vonvol2  46669  snvonmbl  46691  vonsn  46696  iccpartxr  47424  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  intop  48195  assintop  48201  isassintop  48202  ofaddmndmap  48335  rmsupp0  48360  domnmsuppn0  48361  rmsuppss  48362  scmsuppss  48363  gsumlsscl  48372  lincfsuppcl  48406  linccl  48407  lcosn0  48413  lincdifsn  48417  lincsum  48422  lincscm  48423  lincscmcl  48425  islinindfis  48442  lincext1  48447  lincext2  48448  lincext3  48449  lindslinindimp2lem1  48451  lindslinindimp2lem2  48452  lindslinindimp2lem4  48454  lindslinindsimp2lem5  48455  snlindsntor  48464  lincresunitlem2  48469  lincresunit3lem1  48472  lincresunit3lem2  48473  lincresunit3  48474  lincreslvec3  48475  isldepslvec2  48478  zlmodzxzldeplem2  48494  zlmodzxzldeplem3  48495  ldepsnlinclem1  48498  ldepsnlinclem2  48499  1arymaptf1  48635  1arymaptfo  48636  2arympt  48642  2arymaptf1  48646  2arymaptfo  48647  prelrrx2b  48707  eenglngeehlnmlem1  48730  eenglngeehlnmlem2  48731  aacllem  49794