Theorem elmapi 8822

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 8821	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 8812	. . 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 3447  ⟶wf 6507  (class class class)co 7387   ↑_m cmap 8799

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 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

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 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-1st 7968  df-2nd 7969  df-map 8801

This theorem is referenced by:  mapfset  8823  elmapfn  8838  elmapfun  8839  elmapssres  8840  mapsspm  8849  mapfvd  8852  elmapresaun  8853  map0b  8856  mapss  8862  mapsncnv  8866  ralxpmap  8869  mapen  9105  mapxpen  9107  mapunen  9110  mapfienlem1  9356  mapfienlem2  9357  mapfienlem3  9358  mapfien  9359  wemaplem2  9500  wemappo  9502  wemapsolem  9503  wemapso  9504  wemapso2lem  9505  wemapwe  9650  iunmapdisj  9976  fseqenlem1  9977  fseqenlem2  9978  numacn  10002  finacn  10003  acndom  10004  acndom2  10007  infpwfien  10015  infmap2  10170  fin23lem40  10304  isf32lem12  10317  isf34lem6  10333  acncc  10393  pwfseqlem3  10613  pwxpndom2  10618  ramval  16979  ramub  16984  ramcl  17000  prmgaplem7  17028  prmgaplem8  17029  imasdsval2  17479  funcf2  17830  funcpropd  17864  funcestrcsetclem8  18108  funcestrcsetclem9  18109  funcsetcestrclem8  18123  funcsetcestrclem9  18124  mndpsuppss  18692  mndvcl  18724  mndvass  18725  mndvlid  18726  mndvrid  18727  mhmvlin  18728  fsfnn0gsumfsffz  19913  gsummptnn0fzfv  19917  frlmfibas  21671  frlmbas3  21685  frlmipval  21688  frlmphllem  21689  frlmphl  21690  elfilspd  21712  islindf4  21747  psrbagf  21827  mplbas2  21949  ltbwe  21951  psr1baslem  22069  psr1basf  22086  fvcoe1  22092  coe1mul2lem1  22153  ply1coe  22185  mamures  22284  grpvlinv  22285  grpvrinv  22286  mamucl  22288  mamuass  22289  mamudi  22290  mamudir  22291  mamuvs1  22292  mamuvs2  22293  mamulid  22328  mamurid  22329  mattposcl  22340  mattpostpos  22341  tposmap  22344  mamutpos  22345  matgsumcl  22347  mavmulcl  22434  mavmulass  22436  mavmulsolcl  22438  marepvcl  22456  1marepvmarrepid  22462  mdetleib2  22475  mdetf  22482  mdetdiaglem  22485  mdetrlin  22489  mdetrsca  22490  mdetralt  22495  mdetunilem7  22505  mdetunilem9  22507  maducoeval2  22527  madutpos  22529  madugsum  22530  madurid  22531  cramerimplem1  22570  m2pmfzmap  22634  decpmatval  22652  pmatcollpw3lem  22670  pmatcollpw3fi1lem1  22673  pmatcollpw3fi1lem2  22674  pm2mp  22712  chfacfisf  22741  chfacfisfcpmat  22742  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  chfacfpmmulgsum2  22752  cayhamlem1  22753  cpmadugsumlemF  22763  cpmadugsumfi  22764  cayhamlem2  22771  chcoeffeqlem  22772  cayleyhamilton1  22779  pnrmopn  23230  xkoptsub  23541  xkopt  23542  tmdgsum  23982  imasdsf1olem  24261  rrxnm  25291  rrxds  25293  rrxf  25301  rrxmvallem  25304  rrxbasefi  25310  rrxdsfi  25311  ehlbase  25315  ovolscalem2  25415  uniioombl  25490  tdeglem2  25966  plypf1  26117  ulmclm  26296  ulmcaulem  26303  ulmcau  26304  ulmss  26306  ulmbdd  26307  ulmcn  26308  ulmdvlem1  26309  ulmdvlem2  26310  ulmdvlem3  26311  mtest  26313  mtestbdd  26314  mbfulm  26315  iblulm  26316  itgulm  26317  itgulm2  26318  adjval2  31820  fmptco1f1o  32557  fcobijfs  32646  resf1o  32653  fpwrelmap  32656  elrspunidl  33399  elrspunsn  33400  1arithidomlem2  33507  1arithidom  33508  fply1  33527  ply1degltdimlem  33618  fedgmullem1  33625  fedgmul  33627  extdg1id  33661  smatrcl  33786  mbfmf  34244  elmbfmvol2  34258  eulerpartlemelr  34348  eulerpartlemf  34361  eulerpartlemt  34362  eulerpartgbij  34363  eulerpartlemgu  34368  eulerpartlemgh  34369  eulerpartlemgf  34370  eulerpartlemgs2  34371  reprf  34603  reprsuc  34606  vtsprod  34630  circlemethhgt  34634  tgoldbachgtd  34653  satfv1lem  35349  satfvel  35399  satefvfmla0  35405  satefvfmla1  35412  prv1n  35418  mrsubff1  35501  mrsub0  35503  mrsubf  35504  mrsubccat  35505  mrsubcn  35506  msubrn  35516  msubff  35517  msubf  35519  msubff1  35543  mclsind  35557  uncf  37593  curunc  37596  unccur  37597  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  poimir  37647  broucube  37648  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  rrnmet  37823  rrndstprj1  37824  rrndstprj2  37825  rrncmslem  37826  rrnequiv  37829  aks6d1c2lem4  42115  mapcod  42231  evlsvvvallem  42549  evlsvvval  42551  evlselv  42575  fsuppind  42578  mhphf  42585  mapco2g  42702  mapfzcons1  42705  mapfzcons2  42707  mzpcompact2lem  42739  eldiophb  42745  elmapresaunres2  42759  eq0rabdioph  42764  rexrabdioph  42782  eldioph4b  42799  diophren  42801  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  expdioph  43012  pw2f1o2val2  43029  wepwsolem  43031  pwfi2f1o  43085  ofoafo  43345  ofoaid1  43347  ofoaid2  43348  ofoaass  43349  ofoacom  43350  rfovcnvf1od  43993  rfovcnvfvd  43996  fsovrfovd  43998  fsovcnvlem  44002  ntrk0kbimka  44028  neik0pk1imk0  44036  ntrclsfveq1  44049  ntrclsfveq2  44050  ntrclsfveq  44051  ntrclsss  44052  ntrclsiso  44056  ntrclsk2  44057  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  ntrclsk4  44061  ntrneifv3  44071  ntrneineine0lem  44072  ntrneineine1lem  44073  ntrneifv4  44074  ntrneiel2  44075  ntrneicls00  44078  ntrneicls11  44079  ntrneiiso  44080  ntrneik2  44081  ntrneikb  44083  ntrneixb  44084  ntrneik3  44085  ntrneix3  44086  ntrneik13  44087  ntrneix13  44088  ntrneik4w  44089  ntrneik4  44090  clsneifv3  44099  clsneifv4  44100  neicvgfv  44110  k0004ss2  44141  k0004val0  44143  mnringbasefd  44207  mnugrud  44273  mapss2  45199  difmap  45201  inmap  45203  difmapsn  45206  ssmapsn  45210  mccllem  45595  dvnprodlem1  45944  dvnprodlem2  45945  fourierdlem11  46116  fourierdlem12  46117  fourierdlem13  46118  fourierdlem14  46119  fourierdlem34  46139  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  fourierdlem54  46158  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem69  46173  fourierdlem72  46176  fourierdlem74  46178  fourierdlem75  46179  fourierdlem79  46183  fourierdlem85  46189  fourierdlem88  46192  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem92  46196  fourierdlem94  46198  fourierdlem97  46201  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierdlem113  46217  etransclem24  46256  etransclem26  46258  etransclem27  46259  etransclem28  46260  etransclem31  46263  etransclem32  46264  etransclem33  46265  etransclem34  46266  etransclem35  46267  etransclem37  46269  etransclem38  46270  rrxtopnfi  46285  rrndistlt  46288  qndenserrnbllem  46292  rrxsnicc  46298  ioorrnopnlem  46302  subsaliuncl  46356  hoicvr  46546  ovnprodcl  46552  ovnsupge0  46555  ovnlecvr  46556  ovncvrrp  46562  ovn0lem  46563  ovnsubaddlem1  46568  sge0hsphoire  46587  hoidmv1le  46592  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  hoidmvlelem5  46597  hoidmvle  46598  ovnhoilem2  46600  ovnlecvr2  46608  ovncvr2  46609  hoiqssbllem1  46620  hoiqssbllem2  46621  hoiqssbllem3  46622  hspmbllem2  46625  opnvonmbllem2  46631  ovolval2lem  46641  ovolval2  46642  ovolval3  46645  ovolval4lem2  46648  ovolval5lem3  46652  ovnovollem1  46654  ovnovollem2  46655  vonvolmbllem  46658  vonvolmbl2  46661  vonvol2  46662  snvonmbl  46684  vonsn  46689  iccpartxr  47420  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  intop  48191  assintop  48197  isassintop  48198  ofaddmndmap  48331  rmsupp0  48356  domnmsuppn0  48357  rmsuppss  48358  scmsuppss  48359  gsumlsscl  48368  lincfsuppcl  48402  linccl  48403  lcosn0  48409  lincdifsn  48413  lincsum  48418  lincscm  48419  lincscmcl  48421  islinindfis  48438  lincext1  48443  lincext2  48444  lincext3  48445  lindslinindimp2lem1  48447  lindslinindimp2lem2  48448  lindslinindimp2lem4  48450  lindslinindsimp2lem5  48451  snlindsntor  48460  lincresunitlem2  48465  lincresunit3lem1  48468  lincresunit3lem2  48469  lincresunit3  48470  lincreslvec3  48471  isldepslvec2  48474  zlmodzxzldeplem2  48490  zlmodzxzldeplem3  48491  ldepsnlinclem1  48494  ldepsnlinclem2  48495  1arymaptf1  48631  1arymaptfo  48632  2arympt  48638  2arymaptf1  48642  2arymaptfo  48643  prelrrx2b  48703  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  aacllem  49790