Theorem elmapi 8872

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2144  Vcvv 3450  ⟶wf 6534  (class class class)co 7420   ↑_m cmap 8850

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1st 8001  df-2nd 8002  df-map 8852

This theorem is used by:  elmaprd  8873  mapfset  8875  elmapfn  8890  elmapfun  8891  uncf  8894  elmapssres  8897  mapsspm  8907  mapfvd  8910  elmapresaun  8911  map0b  8914  mapss  8920  mapsncnv  8924  ralxpmap  8927  mapen  9163  mapxpen  9165  mapunen  9168  mapfienlem1  9400  mapfienlem2  9401  mapfienlem3  9402  mapfien  9403  wemaplem2  9544  wemappo  9546  wemapsolem  9547  wemapso  9548  wemapso2lem  9549  wemapwe  9701  iunmapdisj  10105  fseqenlem1  10106  fseqenlem2  10107  numacn  10131  finacn  10132  acndom  10133  acndom2  10136  infpwfien  10144  infmap2  10298  fin23lem40  10432  isf32lem12  10445  isf34lem6  10461  acncc  10521  pwfseqlem3  10748  pwxpndom2  10753  s3rex  15106  ramval  17191  ramub  17196  ramcl  17212  prmgaplem7  17240  prmgaplem8  17241  imasdsval2  17693  funcf2  18048  funcpropd  18082  funcestrcsetclem8  18326  funcestrcsetclem9  18327  funcsetcestrclem8  18341  funcsetcestrclem9  18342  mndpsuppss  18964  mndvcl  18997  mndvass  18998  mndvlid  18999  mndvrid  19000  mhmvlin  19001  fsfnn0gsumfsffz  20202  gsummptnn0fzfv  20206  frlmfibas  22073  frlmbas3  22087  frlmipval  22090  frlmphllem  22091  frlmphl  22092  elfilspd  22114  islindf4  22149  psrbagf  22231  mplbas2  22356  ltbwe  22358  evlsvvvallem  22405  evlsvvval  22407  psr1baslem  22508  psr1basf  22524  fvcoe1  22530  coe1mul2lem1  22591  ply1coe  22621  mamures  22717  grpvlinv  22718  grpvrinv  22719  mamucl  22721  mamuass  22722  mamudi  22723  mamudir  22724  mamuvs1  22725  mamuvs2  22726  mamulid  22761  mamurid  22762  mattposcl  22773  mattpostpos  22774  tposmap  22777  mamutpos  22778  matgsumcl  22780  mavmulcl  22867  mavmulass  22869  mavmulsolcl  22871  marepvcl  22889  1marepvmarrepid  22895  mdetleib2  22908  mdetf  22915  mdetdiaglem  22918  mdetrlin  22922  mdetrsca  22923  mdetralt  22928  mdetunilem7  22938  mdetunilem9  22940  maducoeval2  22960  madutpos  22962  madugsum  22963  madurid  22964  matunitlindflem1  22999  matunitlindflem2  23000  cramerimplem1  23006  m2pmfzmap  23070  decpmatval  23088  pmatcollpw3lem  23106  pmatcollpw3fi1lem1  23109  pmatcollpw3fi1lem2  23110  pm2mp  23148  chfacfisf  23177  chfacfisfcpmat  23178  chfacfscmulgsum  23183  chfacfpmmulgsum  23187  chfacfpmmulgsum2  23188  cayhamlem1  23189  cpmadugsumlemF  23199  cpmadugsumfi  23200  cayhamlem2  23207  chcoeffeqlem  23208  cayleyhamilton1  23215  pnrmopn  23666  xkoptsub  23978  xkopt  23979  tmdgsum  24419  imasdsf1olem  24697  rrxnm  25717  rrxds  25719  rrxf  25727  rrxmvallem  25730  rrxbasefi  25736  rrxdsfi  25737  ehlbase  25741  ovolscalem2  25840  uniioombl  25915  tdeglem2  26384  plypf1  26536  ulmclm  26719  ulmcaulem  26726  ulmcau  26727  ulmss  26729  ulmbdd  26730  ulmcn  26731  ulmdvlem1  26732  ulmdvlem2  26733  ulmdvlem3  26734  mtest  26736  mtestbdd  26737  mbfulm  26738  iblulm  26739  itgulm  26740  itgulm2  26741  adjval2  32498  fmptco1f1o  33274  fcobijfs  33359  fcobijfs2  33360  resf1o  33368  fpwrelmap  33371  elrspunidl  34024  elrspunsn  34025  1arithidomlem2  34114  1arithidom  34115  fply1  34136  psrbasfsupp  34189  selvply1rhmlemb  34197  ply1degltdimlem  34300  fedgmullem1  34307  fedgmul  34309  extdg1id  34344  smatrcl  34474  mbfmf  34933  elmbfmvol2  34945  eulerpartlemelr  35035  eulerpartlemf  35048  eulerpartlemt  35049  eulerpartgbij  35050  eulerpartlemgu  35055  eulerpartlemgh  35056  eulerpartlemgf  35057  eulerpartlemgs2  35058  reprf  35287  reprsuc  35290  vtsprod  35314  circlemethhgt  35318  tgoldbachgtd  35337  satfv1lem  36213  satfvel  36263  satefvfmla0  36269  satefvfmla1  36276  prv1n  36282  mrsubff1  36365  mrsub0  36367  mrsubf  36368  mrsubccat  36369  mrsubcn  36370  msubrn  36380  msubff  36381  msubf  36383  msubff1  36407  mclsind  36421  curunc  38618  unccur  38619  poimirlem4  38635  poimirlem5  38636  poimirlem6  38637  poimirlem7  38638  poimirlem8  38639  poimirlem10  38641  poimirlem11  38642  poimirlem12  38643  poimirlem16  38647  poimirlem17  38648  poimirlem18  38649  poimirlem19  38650  poimirlem20  38651  poimirlem21  38652  poimirlem22  38653  poimirlem25  38656  poimirlem26  38657  poimirlem27  38658  poimirlem29  38660  poimirlem30  38661  poimirlem31  38662  poimirlem32  38663  poimir  38664  broucube  38665  mblfinlem3  38670  mblfinlem4  38671  ismblfin  38672  rrnmet  38856  rrndstprj1  38857  rrndstprj2  38858  rrncmslem  38859  rrnequiv  38862  aks6d1c2lem4  43270  mapcod  43387  evlselv  43710  fsuppind  43711  mhphf  43718  mapco2g  43818  mapfzcons1  43821  mapfzcons2  43823  mzpcompact2lem  43855  eldiophb  43861  elmapresaunres2  43875  eq0rabdioph  43880  rexrabdioph  43894  eldioph4b  43911  diophren  43913  rmydioph  44114  rmxdioph  44116  expdiophlem2  44122  expdioph  44123  pw2f1o2val2  44140  wepwsolem  44142  pwfi2f1o  44191  ofoafo  44451  ofoaid1  44453  ofoaid2  44454  ofoaass  44455  ofoacom  44456  rfovcnvf1od  45097  rfovcnvfvd  45100  fsovrfovd  45102  fsovcnvlem  45106  ntrk0kbimka  45132  neik0pk1imk0  45140  ntrclsfveq1  45153  ntrclsfveq2  45154  ntrclsfveq  45155  ntrclsss  45156  ntrclsiso  45160  ntrclsk2  45161  ntrclskb  45162  ntrclsk3  45163  ntrclsk13  45164  ntrclsk4  45165  ntrneifv3  45175  ntrneineine0lem  45176  ntrneineine1lem  45177  ntrneifv4  45178  ntrneiel2  45179  ntrneicls00  45182  ntrneicls11  45183  ntrneiiso  45184  ntrneik2  45185  ntrneikb  45187  ntrneixb  45188  ntrneik3  45189  ntrneix3  45190  ntrneik13  45191  ntrneix13  45192  ntrneik4w  45193  ntrneik4  45194  clsneifv3  45203  clsneifv4  45204  neicvgfv  45214  k0004ss2  45245  k0004val0  45247  mnringbasefd  45309  mnugrud  45361  mapss2  46312  difmap  46313  inmap  46315  difmapsn  46318  ssmapsn  46322  mccllem  46702  dvnprodlem1  47049  dvnprodlem2  47050  fourierdlem11  47221  fourierdlem12  47222  fourierdlem13  47223  fourierdlem14  47224  fourierdlem34  47244  fourierdlem41  47251  fourierdlem48  47257  fourierdlem49  47258  fourierdlem54  47263  fourierdlem63  47272  fourierdlem64  47273  fourierdlem65  47274  fourierdlem69  47278  fourierdlem72  47281  fourierdlem74  47283  fourierdlem75  47284  fourierdlem79  47288  fourierdlem85  47294  fourierdlem88  47297  fourierdlem89  47298  fourierdlem90  47299  fourierdlem91  47300  fourierdlem92  47301  fourierdlem94  47303  fourierdlem97  47306  fourierdlem103  47312  fourierdlem104  47313  fourierdlem111  47320  fourierdlem113  47322  etransclem24  47361  etransclem26  47363  etransclem27  47364  etransclem28  47365  etransclem31  47368  etransclem32  47369  etransclem33  47370  etransclem34  47371  etransclem35  47372  etransclem37  47374  etransclem38  47375  rrxtopnfi  47390  rrndistlt  47393  qndenserrnbllem  47397  rrxsnicc  47403  ioorrnopnlem  47407  subsaliuncl  47461  hoicvr  47651  ovnprodcl  47657  ovnsupge0  47660  ovnlecvr  47661  ovncvrrp  47667  ovn0lem  47668  ovnsubaddlem1  47673  sge0hsphoire  47692  hoidmv1le  47697  hoidmvlelem1  47698  hoidmvlelem2  47699  hoidmvlelem3  47700  hoidmvlelem4  47701  hoidmvlelem5  47702  hoidmvle  47703  ovnhoilem2  47705  ovnlecvr2  47713  ovncvr2  47714  hoiqssbllem1  47725  hoiqssbllem2  47726  hoiqssbllem3  47727  hspmbllem2  47730  opnvonmbllem2  47736  ovolval2lem  47746  ovolval2  47747  ovolval3  47750  ovolval4lem2  47753  ovolval5lem3  47757  ovnovollem1  47759  ovnovollem2  47760  vonvolmbllem  47763  vonvolmbl2  47766  vonvol2  47767  snvonmbl  47789  vonsn  47794  tmachlem-agreeprod  48040  tmachlem-tpopen  48044  iccpartxr  48594  nnsum4primeseven  48991  nnsum4primesevenALTV  48992  intop  49393  assintop  49399  isassintop  49400  ofaddmndmap  49548  rmsupp0  49573  domnmsuppn0  49574  rmsuppss  49575  scmsuppss  49576  gsumlsscl  49585  lincfsuppcl  49618  linccl  49619  lcosn0  49625  lincdifsn  49629  lincsum  49634  lincscm  49635  lincscmcl  49637  islinindfis  49654  lincext1  49659  lincext2  49660  lincext3  49661  lindslinindimp2lem1  49663  lindslinindimp2lem2  49664  lindslinindimp2lem4  49666  lindslinindsimp2lem5  49667  snlindsntor  49676  lincresunitlem2  49681  lincresunit3lem1  49684  lincresunit3lem2  49685  lincresunit3  49686  lincreslvec3  49687  isldepslvec2  49690  zlmodzxzldeplem2  49706  zlmodzxzldeplem3  49707  ldepsnlinclem1  49710  ldepsnlinclem2  49711  1arymaptf1  49847  1arymaptfo  49848  2arympt  49854  2arymaptf1  49858  2arymaptfo  49859  eenglngeehlnmlem1  49943  eenglngeehlnmlem2  49944  aacllem  51107  rr3fvcl  51114  crosspdotsumlem  51132  crossp3d  51135