Theorem elmapi 8428

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∈ wcel 2114  Vcvv 3494  ⟶wf 6351  (class class class)co 7156   ↑_m cmap 8406

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161  df-1st 7689  df-2nd 7690  df-map 8408

This theorem is referenced by:  elmapfn  8429  elmapfun  8430  elmapssres  8431  mapsspm  8440  mapfvd  8443  elmapresaun  8444  map0b  8447  mapss  8453  mapsncnv  8457  ralxpmap  8460  mapen  8681  mapxpen  8683  mapunen  8686  mapfienlem1  8868  mapfienlem2  8869  mapfienlem3  8870  mapfien  8871  wemaplem2  9011  wemappo  9013  wemapsolem  9014  wemapso  9015  wemapso2lem  9016  wemapwe  9160  iunmapdisj  9449  fseqenlem1  9450  fseqenlem2  9451  numacn  9475  finacn  9476  acndom  9477  acndom2  9480  infpwfien  9488  infmap2  9640  fin23lem40  9773  isf32lem12  9786  isf34lem6  9802  acncc  9862  pwfseqlem3  10082  pwxpndom2  10087  ramval  16344  ramub  16349  ramcl  16365  prmgaplem7  16393  prmgaplem8  16394  imasdsval2  16789  funcf2  17138  funcpropd  17170  funcestrcsetclem8  17397  funcestrcsetclem9  17398  funcsetcestrclem8  17412  funcsetcestrclem9  17413  fsfnn0gsumfsffz  19103  gsummptnn0fzfv  19107  mplbas2  20251  ltbwe  20253  psr1baslem  20353  psr1basf  20369  fvcoe1  20375  coe1mul2lem1  20435  ply1coe  20464  frlmfibas  20906  frlmbas3  20920  frlmipval  20923  frlmphllem  20924  frlmphl  20925  elfilspd  20947  islindf4  20982  mamures  21001  mndvcl  21002  mndvass  21003  mndvlid  21004  mndvrid  21005  grpvlinv  21006  grpvrinv  21007  mhmvlin  21008  mamucl  21010  mamuass  21011  mamudi  21012  mamudir  21013  mamuvs1  21014  mamuvs2  21015  mamulid  21050  mamurid  21051  mattposcl  21062  mattpostpos  21063  tposmap  21066  mamutpos  21067  matgsumcl  21069  mavmulcl  21156  mavmulass  21158  mavmulsolcl  21160  marepvcl  21178  1marepvmarrepid  21184  mdetleib2  21197  mdetf  21204  mdetdiaglem  21207  mdetrlin  21211  mdetrsca  21212  mdetralt  21217  mdetunilem7  21227  mdetunilem9  21229  maducoeval2  21249  madutpos  21251  madugsum  21252  madurid  21253  cramerimplem1  21292  m2pmfzmap  21355  decpmatval  21373  pmatcollpw3lem  21391  pmatcollpw3fi1lem1  21394  pmatcollpw3fi1lem2  21395  pm2mp  21433  chfacfisf  21462  chfacfisfcpmat  21463  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  chfacfpmmulgsum2  21473  cayhamlem1  21474  cpmadugsumlemF  21484  cpmadugsumfi  21485  cayhamlem2  21492  chcoeffeqlem  21493  cayleyhamilton1  21500  pnrmopn  21951  xkoptsub  22262  xkopt  22263  tmdgsum  22703  imasdsf1olem  22983  rrxnm  23994  rrxds  23996  rrxf  24004  rrxmvallem  24007  rrxbasefi  24013  rrxdsfi  24014  ehlbase  24018  ovolscalem2  24115  uniioombl  24190  tdeglem2  24655  plypf1  24802  ulmclm  24975  ulmcaulem  24982  ulmcau  24983  ulmss  24985  ulmbdd  24986  ulmcn  24987  ulmdvlem1  24988  ulmdvlem2  24989  ulmdvlem3  24990  mtest  24992  mtestbdd  24993  mbfulm  24994  iblulm  24995  itgulm  24996  itgulm2  24997  adjval2  29668  fmptco1f1o  30378  fcobijfs  30459  resf1o  30466  fpwrelmap  30469  fply1  30931  fedgmullem1  31025  fedgmul  31027  extdg1id  31053  smatrcl  31061  mbfmf  31513  elmbfmvol2  31525  eulerpartlemelr  31615  eulerpartlemf  31628  eulerpartlemt  31629  eulerpartgbij  31630  eulerpartlemgu  31635  eulerpartlemgh  31636  eulerpartlemgf  31637  eulerpartlemgs2  31638  reprf  31883  reprsuc  31886  vtsprod  31910  circlemethhgt  31914  tgoldbachgtd  31933  satfv1lem  32609  satfvel  32659  satefvfmla0  32665  satefvfmla1  32672  prv1n  32678  mrsubff1  32761  mrsub0  32763  mrsubf  32764  mrsubccat  32765  mrsubcn  32766  msubrn  32776  msubff  32777  msubf  32779  msubff1  32803  mclsind  32817  uncf  34886  curunc  34889  unccur  34890  matunitlindflem1  34903  matunitlindflem2  34904  poimirlem4  34911  poimirlem5  34912  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem10  34917  poimirlem11  34918  poimirlem12  34919  poimirlem16  34923  poimirlem17  34924  poimirlem18  34925  poimirlem19  34926  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  poimirlem32  34939  poimir  34940  broucube  34941  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  rrnmet  35122  rrndstprj1  35123  rrndstprj2  35124  rrncmslem  35125  rrnequiv  35128  mapco2g  39360  mapfzcons1  39363  mapfzcons2  39365  mzpcompact2lem  39397  eldiophb  39403  elmapresaunres2  39417  eq0rabdioph  39422  rexrabdioph  39440  eldioph4b  39457  diophren  39459  rmydioph  39660  rmxdioph  39662  expdiophlem2  39668  expdioph  39669  pw2f1o2val2  39686  wepwsolem  39691  pwfi2f1o  39745  rfovcnvf1od  40399  rfovcnvfvd  40402  fsovrfovd  40404  fsovcnvlem  40408  ntrk0kbimka  40438  neik0pk1imk0  40446  ntrclsfveq1  40459  ntrclsfveq2  40460  ntrclsfveq  40461  ntrclsss  40462  ntrclsiso  40466  ntrclsk2  40467  ntrclskb  40468  ntrclsk3  40469  ntrclsk13  40470  ntrclsk4  40471  ntrneifv3  40481  ntrneineine0lem  40482  ntrneineine1lem  40483  ntrneifv4  40484  ntrneiel2  40485  ntrneicls00  40488  ntrneicls11  40489  ntrneiiso  40490  ntrneik2  40491  ntrneikb  40493  ntrneixb  40494  ntrneik3  40495  ntrneix3  40496  ntrneik13  40497  ntrneix13  40498  ntrneik4w  40499  ntrneik4  40500  clsneifv3  40509  clsneifv4  40510  neicvgfv  40520  k0004ss2  40551  k0004val0  40553  mnugrud  40669  mapss2  41517  difmap  41519  inmap  41521  difmapsn  41524  ssmapsn  41528  mccllem  41927  dvnprodlem1  42280  dvnprodlem2  42281  fourierdlem11  42452  fourierdlem12  42453  fourierdlem13  42454  fourierdlem14  42455  fourierdlem34  42475  fourierdlem41  42482  fourierdlem48  42488  fourierdlem49  42489  fourierdlem54  42494  fourierdlem63  42503  fourierdlem64  42504  fourierdlem65  42505  fourierdlem69  42509  fourierdlem72  42512  fourierdlem74  42514  fourierdlem75  42515  fourierdlem79  42519  fourierdlem85  42525  fourierdlem88  42528  fourierdlem89  42529  fourierdlem90  42530  fourierdlem91  42531  fourierdlem92  42532  fourierdlem94  42534  fourierdlem97  42537  fourierdlem103  42543  fourierdlem104  42544  fourierdlem111  42551  fourierdlem113  42553  etransclem24  42592  etransclem26  42594  etransclem27  42595  etransclem28  42596  etransclem31  42599  etransclem32  42600  etransclem33  42601  etransclem34  42602  etransclem35  42603  etransclem37  42605  etransclem38  42606  rrxtopnfi  42621  rrndistlt  42624  qndenserrnbllem  42628  rrxsnicc  42634  ioorrnopnlem  42638  subsaliuncl  42690  hoicvr  42879  ovnprodcl  42885  ovnsupge0  42888  ovnlecvr  42889  ovncvrrp  42895  ovn0lem  42896  ovnsubaddlem1  42901  sge0hsphoire  42920  hoidmv1le  42925  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem3  42928  hoidmvlelem4  42929  hoidmvlelem5  42930  hoidmvle  42931  ovnhoilem2  42933  ovnlecvr2  42941  ovncvr2  42942  hoiqssbllem1  42953  hoiqssbllem2  42954  hoiqssbllem3  42955  hspmbllem2  42958  opnvonmbllem2  42964  ovolval2lem  42974  ovolval2  42975  ovolval3  42978  ovolval4lem2  42981  ovolval5lem3  42985  ovnovollem1  42987  ovnovollem2  42988  vonvolmbllem  42991  vonvolmbl2  42994  vonvol2  42995  snvonmbl  43017  vonsn  43022  iccpartxr  43628  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  intop  44159  assintop  44165  isassintop  44166  ofaddmndmap  44441  rmsupp0  44465  domnmsuppn0  44466  rmsuppss  44467  mndpsuppss  44468  scmsuppss  44469  gsumlsscl  44480  lincfsuppcl  44517  linccl  44518  lcosn0  44524  lincdifsn  44528  lincsum  44533  lincscm  44534  lincscmcl  44536  islinindfis  44553  lincext1  44558  lincext2  44559  lincext3  44560  lindslinindimp2lem1  44562  lindslinindimp2lem2  44563  lindslinindimp2lem4  44565  lindslinindsimp2lem5  44566  snlindsntor  44575  lincresunitlem2  44580  lincresunit3lem1  44583  lincresunit3lem2  44584  lincresunit3  44585  lincreslvec3  44586  isldepslvec2  44589  zlmodzxzldeplem2  44605  zlmodzxzldeplem3  44606  ldepsnlinclem1  44609  ldepsnlinclem2  44610  prelrrx2b  44750  eenglngeehlnmlem1  44773  eenglngeehlnmlem2  44774  aacllem  44951