Theorem elmapi 8783

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 8782	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 8773	. . 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 3438  ⟶wf 6482  (class class class)co 7353   ↑_m cmap 8760

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 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494  df-ov 7356  df-oprab 7357  df-mpo 7358  df-1st 7931  df-2nd 7932  df-map 8762

This theorem is referenced by:  mapfset  8784  elmapfn  8799  elmapfun  8800  elmapssres  8801  mapsspm  8810  mapfvd  8813  elmapresaun  8814  map0b  8817  mapss  8823  mapsncnv  8827  ralxpmap  8830  mapen  9065  mapxpen  9067  mapunen  9070  mapfienlem1  9314  mapfienlem2  9315  mapfienlem3  9316  mapfien  9317  wemaplem2  9458  wemappo  9460  wemapsolem  9461  wemapso  9462  wemapso2lem  9463  wemapwe  9612  iunmapdisj  9936  fseqenlem1  9937  fseqenlem2  9938  numacn  9962  finacn  9963  acndom  9964  acndom2  9967  infpwfien  9975  infmap2  10130  fin23lem40  10264  isf32lem12  10277  isf34lem6  10293  acncc  10353  pwfseqlem3  10573  pwxpndom2  10578  ramval  16939  ramub  16944  ramcl  16960  prmgaplem7  16988  prmgaplem8  16989  imasdsval2  17439  funcf2  17794  funcpropd  17828  funcestrcsetclem8  18072  funcestrcsetclem9  18073  funcsetcestrclem8  18087  funcsetcestrclem9  18088  mndpsuppss  18658  mndvcl  18690  mndvass  18691  mndvlid  18692  mndvrid  18693  mhmvlin  18694  fsfnn0gsumfsffz  19881  gsummptnn0fzfv  19885  frlmfibas  21688  frlmbas3  21702  frlmipval  21705  frlmphllem  21706  frlmphl  21707  elfilspd  21729  islindf4  21764  psrbagf  21844  mplbas2  21966  ltbwe  21968  psr1baslem  22086  psr1basf  22103  fvcoe1  22109  coe1mul2lem1  22170  ply1coe  22202  mamures  22301  grpvlinv  22302  grpvrinv  22303  mamucl  22305  mamuass  22306  mamudi  22307  mamudir  22308  mamuvs1  22309  mamuvs2  22310  mamulid  22345  mamurid  22346  mattposcl  22357  mattpostpos  22358  tposmap  22361  mamutpos  22362  matgsumcl  22364  mavmulcl  22451  mavmulass  22453  mavmulsolcl  22455  marepvcl  22473  1marepvmarrepid  22479  mdetleib2  22492  mdetf  22499  mdetdiaglem  22502  mdetrlin  22506  mdetrsca  22507  mdetralt  22512  mdetunilem7  22522  mdetunilem9  22524  maducoeval2  22544  madutpos  22546  madugsum  22547  madurid  22548  cramerimplem1  22587  m2pmfzmap  22651  decpmatval  22669  pmatcollpw3lem  22687  pmatcollpw3fi1lem1  22690  pmatcollpw3fi1lem2  22691  pm2mp  22729  chfacfisf  22758  chfacfisfcpmat  22759  chfacfscmulgsum  22764  chfacfpmmulgsum  22768  chfacfpmmulgsum2  22769  cayhamlem1  22770  cpmadugsumlemF  22780  cpmadugsumfi  22781  cayhamlem2  22788  chcoeffeqlem  22789  cayleyhamilton1  22796  pnrmopn  23247  xkoptsub  23558  xkopt  23559  tmdgsum  23999  imasdsf1olem  24278  rrxnm  25308  rrxds  25310  rrxf  25318  rrxmvallem  25321  rrxbasefi  25327  rrxdsfi  25328  ehlbase  25332  ovolscalem2  25432  uniioombl  25507  tdeglem2  25983  plypf1  26134  ulmclm  26313  ulmcaulem  26320  ulmcau  26321  ulmss  26323  ulmbdd  26324  ulmcn  26325  ulmdvlem1  26326  ulmdvlem2  26327  ulmdvlem3  26328  mtest  26330  mtestbdd  26331  mbfulm  26332  iblulm  26333  itgulm  26334  itgulm2  26335  adjval2  31854  fmptco1f1o  32595  fcobijfs  32684  fcobijfs2  32685  resf1o  32692  fpwrelmap  32695  elrspunidl  33384  elrspunsn  33385  1arithidomlem2  33492  1arithidom  33493  fply1  33512  psrbasfsupp  33563  ply1degltdimlem  33608  fedgmullem1  33615  fedgmul  33617  extdg1id  33652  smatrcl  33782  mbfmf  34240  elmbfmvol2  34254  eulerpartlemelr  34344  eulerpartlemf  34357  eulerpartlemt  34358  eulerpartgbij  34359  eulerpartlemgu  34364  eulerpartlemgh  34365  eulerpartlemgf  34366  eulerpartlemgs2  34367  reprf  34599  reprsuc  34602  vtsprod  34626  circlemethhgt  34630  tgoldbachgtd  34649  satfv1lem  35354  satfvel  35404  satefvfmla0  35410  satefvfmla1  35417  prv1n  35423  mrsubff1  35506  mrsub0  35508  mrsubf  35509  mrsubccat  35510  mrsubcn  35511  msubrn  35521  msubff  35522  msubf  35524  msubff1  35548  mclsind  35562  uncf  37598  curunc  37601  unccur  37602  matunitlindflem1  37615  matunitlindflem2  37616  poimirlem4  37623  poimirlem5  37624  poimirlem6  37625  poimirlem7  37626  poimirlem8  37627  poimirlem10  37629  poimirlem11  37630  poimirlem12  37631  poimirlem16  37635  poimirlem17  37636  poimirlem18  37637  poimirlem19  37638  poimirlem20  37639  poimirlem21  37640  poimirlem22  37641  poimirlem25  37644  poimirlem26  37645  poimirlem27  37646  poimirlem29  37648  poimirlem30  37649  poimirlem31  37650  poimirlem32  37651  poimir  37652  broucube  37653  mblfinlem3  37658  mblfinlem4  37659  ismblfin  37660  rrnmet  37828  rrndstprj1  37829  rrndstprj2  37830  rrncmslem  37831  rrnequiv  37834  aks6d1c2lem4  42120  mapcod  42236  evlsvvvallem  42554  evlsvvval  42556  evlselv  42580  fsuppind  42583  mhphf  42590  mapco2g  42707  mapfzcons1  42710  mapfzcons2  42712  mzpcompact2lem  42744  eldiophb  42750  elmapresaunres2  42764  eq0rabdioph  42769  rexrabdioph  42787  eldioph4b  42804  diophren  42806  rmydioph  43007  rmxdioph  43009  expdiophlem2  43015  expdioph  43016  pw2f1o2val2  43033  wepwsolem  43035  pwfi2f1o  43089  ofoafo  43349  ofoaid1  43351  ofoaid2  43352  ofoaass  43353  ofoacom  43354  rfovcnvf1od  43997  rfovcnvfvd  44000  fsovrfovd  44002  fsovcnvlem  44006  ntrk0kbimka  44032  neik0pk1imk0  44040  ntrclsfveq1  44053  ntrclsfveq2  44054  ntrclsfveq  44055  ntrclsss  44056  ntrclsiso  44060  ntrclsk2  44061  ntrclskb  44062  ntrclsk3  44063  ntrclsk13  44064  ntrclsk4  44065  ntrneifv3  44075  ntrneineine0lem  44076  ntrneineine1lem  44077  ntrneifv4  44078  ntrneiel2  44079  ntrneicls00  44082  ntrneicls11  44083  ntrneiiso  44084  ntrneik2  44085  ntrneikb  44087  ntrneixb  44088  ntrneik3  44089  ntrneix3  44090  ntrneik13  44091  ntrneix13  44092  ntrneik4w  44093  ntrneik4  44094  clsneifv3  44103  clsneifv4  44104  neicvgfv  44114  k0004ss2  44145  k0004val0  44147  mnringbasefd  44211  mnugrud  44277  mapss2  45203  difmap  45205  inmap  45207  difmapsn  45210  ssmapsn  45214  mccllem  45598  dvnprodlem1  45947  dvnprodlem2  45948  fourierdlem11  46119  fourierdlem12  46120  fourierdlem13  46121  fourierdlem14  46122  fourierdlem34  46142  fourierdlem41  46149  fourierdlem48  46155  fourierdlem49  46156  fourierdlem54  46161  fourierdlem63  46170  fourierdlem64  46171  fourierdlem65  46172  fourierdlem69  46176  fourierdlem72  46179  fourierdlem74  46181  fourierdlem75  46182  fourierdlem79  46186  fourierdlem85  46192  fourierdlem88  46195  fourierdlem89  46196  fourierdlem90  46197  fourierdlem91  46198  fourierdlem92  46199  fourierdlem94  46201  fourierdlem97  46204  fourierdlem103  46210  fourierdlem104  46211  fourierdlem111  46218  fourierdlem113  46220  etransclem24  46259  etransclem26  46261  etransclem27  46262  etransclem28  46263  etransclem31  46266  etransclem32  46267  etransclem33  46268  etransclem34  46269  etransclem35  46270  etransclem37  46272  etransclem38  46273  rrxtopnfi  46288  rrndistlt  46291  qndenserrnbllem  46295  rrxsnicc  46301  ioorrnopnlem  46305  subsaliuncl  46359  hoicvr  46549  ovnprodcl  46555  ovnsupge0  46558  ovnlecvr  46559  ovncvrrp  46565  ovn0lem  46566  ovnsubaddlem1  46571  sge0hsphoire  46590  hoidmv1le  46595  hoidmvlelem1  46596  hoidmvlelem2  46597  hoidmvlelem3  46598  hoidmvlelem4  46599  hoidmvlelem5  46600  hoidmvle  46601  ovnhoilem2  46603  ovnlecvr2  46611  ovncvr2  46612  hoiqssbllem1  46623  hoiqssbllem2  46624  hoiqssbllem3  46625  hspmbllem2  46628  opnvonmbllem2  46634  ovolval2lem  46644  ovolval2  46645  ovolval3  46648  ovolval4lem2  46651  ovolval5lem3  46655  ovnovollem1  46657  ovnovollem2  46658  vonvolmbllem  46661  vonvolmbl2  46664  vonvol2  46665  snvonmbl  46687  vonsn  46692  iccpartxr  47423  nnsum4primeseven  47804  nnsum4primesevenALTV  47805  intop  48207  assintop  48213  isassintop  48214  ofaddmndmap  48347  rmsupp0  48372  domnmsuppn0  48373  rmsuppss  48374  scmsuppss  48375  gsumlsscl  48384  lincfsuppcl  48418  linccl  48419  lcosn0  48425  lincdifsn  48429  lincsum  48434  lincscm  48435  lincscmcl  48437  islinindfis  48454  lincext1  48459  lincext2  48460  lincext3  48461  lindslinindimp2lem1  48463  lindslinindimp2lem2  48464  lindslinindimp2lem4  48466  lindslinindsimp2lem5  48467  snlindsntor  48476  lincresunitlem2  48481  lincresunit3lem1  48484  lincresunit3lem2  48485  lincresunit3  48486  lincreslvec3  48487  isldepslvec2  48490  zlmodzxzldeplem2  48506  zlmodzxzldeplem3  48507  ldepsnlinclem1  48510  ldepsnlinclem2  48511  1arymaptf1  48647  1arymaptfo  48648  2arympt  48654  2arymaptf1  48658  2arymaptfo  48659  prelrrx2b  48719  eenglngeehlnmlem1  48742  eenglngeehlnmlem2  48743  aacllem  49806