Theorem elmapi 8834

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2145  Vcvv 3457  ⟶wf 6521  (class class class)co 7400   ↑_m cmap 8812

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-1st 7974  df-2nd 7975  df-map 8814

This theorem is referenced by:  mapfset  8835  elmapfn  8850  elmapfun  8851  elmapssres  8852  mapsspm  8862  mapfvd  8865  elmapresaun  8866  map0b  8869  mapss  8875  mapsncnv  8879  ralxpmap  8882  mapen  9117  mapxpen  9119  mapunen  9122  mapfienlem1  9353  mapfienlem2  9354  mapfienlem3  9355  mapfien  9356  wemaplem2  9497  wemappo  9499  wemapsolem  9500  wemapso  9501  wemapso2lem  9502  wemapwe  9654  iunmapdisj  9995  fseqenlem1  9996  fseqenlem2  9997  numacn  10021  finacn  10022  acndom  10023  acndom2  10026  infpwfien  10034  infmap2  10188  fin23lem40  10323  isf32lem12  10336  isf34lem6  10352  acncc  10412  pwfseqlem3  10633  pwxpndom2  10638  ramval  17058  ramub  17063  ramcl  17079  prmgaplem7  17107  prmgaplem8  17108  imasdsval2  17560  funcf2  17915  funcpropd  17949  funcestrcsetclem8  18193  funcestrcsetclem9  18194  funcsetcestrclem8  18208  funcsetcestrclem9  18209  mndpsuppss  18813  mndvcl  18845  mndvass  18846  mndvlid  18847  mndvrid  18848  mhmvlin  18849  fsfnn0gsumfsffz  20044  gsummptnn0fzfv  20048  frlmfibas  21872  frlmbas3  21886  frlmipval  21889  frlmphllem  21890  frlmphl  21891  elfilspd  21913  islindf4  21948  psrbagf  22028  mplbas2  22153  ltbwe  22155  evlsvvvallem  22202  evlsvvval  22204  psr1baslem  22305  psr1basf  22321  fvcoe1  22327  coe1mul2lem1  22388  ply1coe  22419  mamures  22515  grpvlinv  22516  grpvrinv  22517  mamucl  22519  mamuass  22520  mamudi  22521  mamudir  22522  mamuvs1  22523  mamuvs2  22524  mamulid  22559  mamurid  22560  mattposcl  22571  mattpostpos  22572  tposmap  22575  mamutpos  22576  matgsumcl  22578  mavmulcl  22665  mavmulass  22667  mavmulsolcl  22669  marepvcl  22687  1marepvmarrepid  22693  mdetleib2  22706  mdetf  22713  mdetdiaglem  22716  mdetrlin  22720  mdetrsca  22721  mdetralt  22726  mdetunilem7  22736  mdetunilem9  22738  maducoeval2  22758  madutpos  22760  madugsum  22761  madurid  22762  cramerimplem1  22801  m2pmfzmap  22865  decpmatval  22883  pmatcollpw3lem  22901  pmatcollpw3fi1lem1  22904  pmatcollpw3fi1lem2  22905  pm2mp  22943  chfacfisf  22972  chfacfisfcpmat  22973  chfacfscmulgsum  22978  chfacfpmmulgsum  22982  chfacfpmmulgsum2  22983  cayhamlem1  22984  cpmadugsumlemF  22994  cpmadugsumfi  22995  cayhamlem2  23002  chcoeffeqlem  23003  cayleyhamilton1  23010  pnrmopn  23461  xkoptsub  23772  xkopt  23773  tmdgsum  24213  imasdsf1olem  24491  rrxnm  25511  rrxds  25513  rrxf  25521  rrxmvallem  25524  rrxbasefi  25530  rrxdsfi  25531  ehlbase  25535  ovolscalem2  25634  uniioombl  25709  tdeglem2  26179  plypf1  26330  ulmclm  26508  ulmcaulem  26515  ulmcau  26516  ulmss  26518  ulmbdd  26519  ulmcn  26520  ulmdvlem1  26521  ulmdvlem2  26522  ulmdvlem3  26523  mtest  26525  mtestbdd  26526  mbfulm  26527  iblulm  26528  itgulm  26529  itgulm2  26530  adjval2  32152  fmptco1f1o  32890  fcobijfs  32978  fcobijfs2  32979  resf1o  32987  fpwrelmap  32990  elrspunidl  33652  elrspunsn  33653  1arithidomlem2  33743  1arithidom  33744  fply1  33765  psrbasfsupp  33818  selvply1rhmlemb  33826  ply1degltdimlem  33929  fedgmullem1  33936  fedgmul  33938  extdg1id  33973  smatrcl  34103  mbfmf  34561  elmbfmvol2  34574  eulerpartlemelr  34664  eulerpartlemf  34677  eulerpartlemt  34678  eulerpartgbij  34679  eulerpartlemgu  34684  eulerpartlemgh  34685  eulerpartlemgf  34686  eulerpartlemgs2  34687  reprf  34916  reprsuc  34919  vtsprod  34943  circlemethhgt  34947  tgoldbachgtd  34966  satfv1lem  35725  satfvel  35775  satefvfmla0  35781  satefvfmla1  35788  prv1n  35794  mrsubff1  35877  mrsub0  35879  mrsubf  35880  mrsubccat  35881  mrsubcn  35882  msubrn  35892  msubff  35893  msubf  35895  msubff1  35919  mclsind  35933  uncf  38110  curunc  38113  unccur  38114  matunitlindflem1  38127  matunitlindflem2  38128  poimirlem4  38135  poimirlem5  38136  poimirlem6  38137  poimirlem7  38138  poimirlem8  38139  poimirlem10  38141  poimirlem11  38142  poimirlem12  38143  poimirlem16  38147  poimirlem17  38148  poimirlem18  38149  poimirlem19  38150  poimirlem20  38151  poimirlem21  38152  poimirlem22  38153  poimirlem25  38156  poimirlem26  38157  poimirlem27  38158  poimirlem29  38160  poimirlem30  38161  poimirlem31  38162  poimirlem32  38163  poimir  38164  broucube  38165  mblfinlem3  38170  mblfinlem4  38171  ismblfin  38172  rrnmet  38340  rrndstprj1  38341  rrndstprj2  38342  rrncmslem  38343  rrnequiv  38346  aks6d1c2lem4  42756  mapcod  42871  evlselv  43183  fsuppind  43184  mhphf  43191  mapco2g  43307  mapfzcons1  43310  mapfzcons2  43312  mzpcompact2lem  43344  eldiophb  43350  elmapresaunres2  43364  eq0rabdioph  43369  rexrabdioph  43383  eldioph4b  43400  diophren  43402  rmydioph  43603  rmxdioph  43605  expdiophlem2  43611  expdioph  43612  pw2f1o2val2  43629  wepwsolem  43631  pwfi2f1o  43685  ofoafo  43945  ofoaid1  43947  ofoaid2  43948  ofoaass  43949  ofoacom  43950  rfovcnvf1od  44592  rfovcnvfvd  44595  fsovrfovd  44597  fsovcnvlem  44601  ntrk0kbimka  44627  neik0pk1imk0  44635  ntrclsfveq1  44648  ntrclsfveq2  44649  ntrclsfveq  44650  ntrclsss  44651  ntrclsiso  44655  ntrclsk2  44656  ntrclskb  44657  ntrclsk3  44658  ntrclsk13  44659  ntrclsk4  44660  ntrneifv3  44670  ntrneineine0lem  44671  ntrneineine1lem  44672  ntrneifv4  44673  ntrneiel2  44674  ntrneicls00  44677  ntrneicls11  44678  ntrneiiso  44679  ntrneik2  44680  ntrneikb  44682  ntrneixb  44683  ntrneik3  44684  ntrneix3  44685  ntrneik13  44686  ntrneix13  44687  ntrneik4w  44688  ntrneik4  44689  clsneifv3  44698  clsneifv4  44699  neicvgfv  44709  k0004ss2  44740  k0004val0  44742  mnringbasefd  44806  mnugrud  44858  mapss2  45780  difmap  45781  inmap  45783  difmapsn  45786  ssmapsn  45790  mccllem  46171  dvnprodlem1  46518  dvnprodlem2  46519  fourierdlem11  46690  fourierdlem12  46691  fourierdlem13  46692  fourierdlem14  46693  fourierdlem34  46713  fourierdlem41  46720  fourierdlem48  46726  fourierdlem49  46727  fourierdlem54  46732  fourierdlem63  46741  fourierdlem64  46742  fourierdlem65  46743  fourierdlem69  46747  fourierdlem72  46750  fourierdlem74  46752  fourierdlem75  46753  fourierdlem79  46757  fourierdlem85  46763  fourierdlem88  46766  fourierdlem89  46767  fourierdlem90  46768  fourierdlem91  46769  fourierdlem92  46770  fourierdlem94  46772  fourierdlem97  46775  fourierdlem103  46781  fourierdlem104  46782  fourierdlem111  46789  fourierdlem113  46791  etransclem24  46830  etransclem26  46832  etransclem27  46833  etransclem28  46834  etransclem31  46837  etransclem32  46838  etransclem33  46839  etransclem34  46840  etransclem35  46841  etransclem37  46843  etransclem38  46844  rrxtopnfi  46859  rrndistlt  46862  qndenserrnbllem  46866  rrxsnicc  46872  ioorrnopnlem  46876  subsaliuncl  46930  hoicvr  47120  ovnprodcl  47126  ovnsupge0  47129  ovnlecvr  47130  ovncvrrp  47136  ovn0lem  47137  ovnsubaddlem1  47142  sge0hsphoire  47161  hoidmv1le  47166  hoidmvlelem1  47167  hoidmvlelem2  47168  hoidmvlelem3  47169  hoidmvlelem4  47170  hoidmvlelem5  47171  hoidmvle  47172  ovnhoilem2  47174  ovnlecvr2  47182  ovncvr2  47183  hoiqssbllem1  47194  hoiqssbllem2  47195  hoiqssbllem3  47196  hspmbllem2  47199  opnvonmbllem2  47205  ovolval2lem  47215  ovolval2  47216  ovolval3  47219  ovolval4lem2  47222  ovolval5lem3  47226  ovnovollem1  47228  ovnovollem2  47229  vonvolmbllem  47232  vonvolmbl2  47235  vonvol2  47236  snvonmbl  47258  vonsn  47263  iccpartxr  48023  nnsum4primeseven  48420  nnsum4primesevenALTV  48421  intop  48823  assintop  48829  isassintop  48830  ofaddmndmap  48974  rmsupp0  48999  domnmsuppn0  49000  rmsuppss  49001  scmsuppss  49002  gsumlsscl  49011  lincfsuppcl  49044  linccl  49045  lcosn0  49051  lincdifsn  49055  lincsum  49060  lincscm  49061  lincscmcl  49063  islinindfis  49080  lincext1  49085  lincext2  49086  lincext3  49087  lindslinindimp2lem1  49089  lindslinindimp2lem2  49090  lindslinindimp2lem4  49092  lindslinindsimp2lem5  49093  snlindsntor  49102  lincresunitlem2  49107  lincresunit3lem1  49110  lincresunit3lem2  49111  lincresunit3  49112  lincreslvec3  49113  isldepslvec2  49116  zlmodzxzldeplem2  49132  zlmodzxzldeplem3  49133  ldepsnlinclem1  49136  ldepsnlinclem2  49137  1arymaptf1  49273  1arymaptfo  49274  2arympt  49280  2arymaptf1  49284  2arymaptfo  49285  prelrrx2b  49345  eenglngeehlnmlem1  49368  eenglngeehlnmlem2  49369  aacllem  50430