Theorem elmapi 8773

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 8772	. . 3 ⊢ (𝐴 ∈ (𝐵 ↑m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2		elmapg 8763	. . 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 2111  Vcvv 3436  ⟶wf 6477  (class class class)co 7346   ↑_m cmap 8750

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-iun 4943  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489  df-ov 7349  df-oprab 7350  df-mpo 7351  df-1st 7921  df-2nd 7922  df-map 8752

This theorem is referenced by:  mapfset  8774  elmapfn  8789  elmapfun  8790  elmapssres  8791  mapsspm  8800  mapfvd  8803  elmapresaun  8804  map0b  8807  mapss  8813  mapsncnv  8817  ralxpmap  8820  mapen  9054  mapxpen  9056  mapunen  9059  mapfienlem1  9289  mapfienlem2  9290  mapfienlem3  9291  mapfien  9292  wemaplem2  9433  wemappo  9435  wemapsolem  9436  wemapso  9437  wemapso2lem  9438  wemapwe  9587  iunmapdisj  9911  fseqenlem1  9912  fseqenlem2  9913  numacn  9937  finacn  9938  acndom  9939  acndom2  9942  infpwfien  9950  infmap2  10105  fin23lem40  10239  isf32lem12  10252  isf34lem6  10268  acncc  10328  pwfseqlem3  10548  pwxpndom2  10553  ramval  16917  ramub  16922  ramcl  16938  prmgaplem7  16966  prmgaplem8  16967  imasdsval2  17417  funcf2  17772  funcpropd  17806  funcestrcsetclem8  18050  funcestrcsetclem9  18051  funcsetcestrclem8  18065  funcsetcestrclem9  18066  mndpsuppss  18670  mndvcl  18702  mndvass  18703  mndvlid  18704  mndvrid  18705  mhmvlin  18706  fsfnn0gsumfsffz  19893  gsummptnn0fzfv  19897  frlmfibas  21697  frlmbas3  21711  frlmipval  21714  frlmphllem  21715  frlmphl  21716  elfilspd  21738  islindf4  21773  psrbagf  21853  mplbas2  21975  ltbwe  21977  psr1baslem  22095  psr1basf  22112  fvcoe1  22118  coe1mul2lem1  22179  ply1coe  22211  mamures  22310  grpvlinv  22311  grpvrinv  22312  mamucl  22314  mamuass  22315  mamudi  22316  mamudir  22317  mamuvs1  22318  mamuvs2  22319  mamulid  22354  mamurid  22355  mattposcl  22366  mattpostpos  22367  tposmap  22370  mamutpos  22371  matgsumcl  22373  mavmulcl  22460  mavmulass  22462  mavmulsolcl  22464  marepvcl  22482  1marepvmarrepid  22488  mdetleib2  22501  mdetf  22508  mdetdiaglem  22511  mdetrlin  22515  mdetrsca  22516  mdetralt  22521  mdetunilem7  22531  mdetunilem9  22533  maducoeval2  22553  madutpos  22555  madugsum  22556  madurid  22557  cramerimplem1  22596  m2pmfzmap  22660  decpmatval  22678  pmatcollpw3lem  22696  pmatcollpw3fi1lem1  22699  pmatcollpw3fi1lem2  22700  pm2mp  22738  chfacfisf  22767  chfacfisfcpmat  22768  chfacfscmulgsum  22773  chfacfpmmulgsum  22777  chfacfpmmulgsum2  22778  cayhamlem1  22779  cpmadugsumlemF  22789  cpmadugsumfi  22790  cayhamlem2  22797  chcoeffeqlem  22798  cayleyhamilton1  22805  pnrmopn  23256  xkoptsub  23567  xkopt  23568  tmdgsum  24008  imasdsf1olem  24286  rrxnm  25316  rrxds  25318  rrxf  25326  rrxmvallem  25329  rrxbasefi  25335  rrxdsfi  25336  ehlbase  25340  ovolscalem2  25440  uniioombl  25515  tdeglem2  25991  plypf1  26142  ulmclm  26321  ulmcaulem  26328  ulmcau  26329  ulmss  26331  ulmbdd  26332  ulmcn  26333  ulmdvlem1  26334  ulmdvlem2  26335  ulmdvlem3  26336  mtest  26338  mtestbdd  26339  mbfulm  26340  iblulm  26341  itgulm  26342  itgulm2  26343  adjval2  31866  fmptco1f1o  32610  fcobijfs  32699  fcobijfs2  32700  resf1o  32708  fpwrelmap  32711  elrspunidl  33388  elrspunsn  33389  1arithidomlem2  33496  1arithidom  33497  fply1  33516  psrbasfsupp  33567  ply1degltdimlem  33630  fedgmullem1  33637  fedgmul  33639  extdg1id  33674  smatrcl  33804  mbfmf  34262  elmbfmvol2  34275  eulerpartlemelr  34365  eulerpartlemf  34378  eulerpartlemt  34379  eulerpartgbij  34380  eulerpartlemgu  34385  eulerpartlemgh  34386  eulerpartlemgf  34387  eulerpartlemgs2  34388  reprf  34620  reprsuc  34623  vtsprod  34647  circlemethhgt  34651  tgoldbachgtd  34670  satfv1lem  35394  satfvel  35444  satefvfmla0  35450  satefvfmla1  35457  prv1n  35463  mrsubff1  35546  mrsub0  35548  mrsubf  35549  mrsubccat  35550  mrsubcn  35551  msubrn  35561  msubff  35562  msubf  35564  msubff1  35588  mclsind  35602  uncf  37638  curunc  37641  unccur  37642  matunitlindflem1  37655  matunitlindflem2  37656  poimirlem4  37663  poimirlem5  37664  poimirlem6  37665  poimirlem7  37666  poimirlem8  37667  poimirlem10  37669  poimirlem11  37670  poimirlem12  37671  poimirlem16  37675  poimirlem17  37676  poimirlem18  37677  poimirlem19  37678  poimirlem20  37679  poimirlem21  37680  poimirlem22  37681  poimirlem25  37684  poimirlem26  37685  poimirlem27  37686  poimirlem29  37688  poimirlem30  37689  poimirlem31  37690  poimirlem32  37691  poimir  37692  broucube  37693  mblfinlem3  37698  mblfinlem4  37699  ismblfin  37700  rrnmet  37868  rrndstprj1  37869  rrndstprj2  37870  rrncmslem  37871  rrnequiv  37874  aks6d1c2lem4  42159  mapcod  42275  evlsvvvallem  42593  evlsvvval  42595  evlselv  42619  fsuppind  42622  mhphf  42629  mapco2g  42746  mapfzcons1  42749  mapfzcons2  42751  mzpcompact2lem  42783  eldiophb  42789  elmapresaunres2  42803  eq0rabdioph  42808  rexrabdioph  42826  eldioph4b  42843  diophren  42845  rmydioph  43046  rmxdioph  43048  expdiophlem2  43054  expdioph  43055  pw2f1o2val2  43072  wepwsolem  43074  pwfi2f1o  43128  ofoafo  43388  ofoaid1  43390  ofoaid2  43391  ofoaass  43392  ofoacom  43393  rfovcnvf1od  44036  rfovcnvfvd  44039  fsovrfovd  44041  fsovcnvlem  44045  ntrk0kbimka  44071  neik0pk1imk0  44079  ntrclsfveq1  44092  ntrclsfveq2  44093  ntrclsfveq  44094  ntrclsss  44095  ntrclsiso  44099  ntrclsk2  44100  ntrclskb  44101  ntrclsk3  44102  ntrclsk13  44103  ntrclsk4  44104  ntrneifv3  44114  ntrneineine0lem  44115  ntrneineine1lem  44116  ntrneifv4  44117  ntrneiel2  44118  ntrneicls00  44121  ntrneicls11  44122  ntrneiiso  44123  ntrneik2  44124  ntrneikb  44126  ntrneixb  44127  ntrneik3  44128  ntrneix3  44129  ntrneik13  44130  ntrneix13  44131  ntrneik4w  44132  ntrneik4  44133  clsneifv3  44142  clsneifv4  44143  neicvgfv  44153  k0004ss2  44184  k0004val0  44186  mnringbasefd  44250  mnugrud  44316  mapss2  45241  difmap  45243  inmap  45245  difmapsn  45248  ssmapsn  45252  mccllem  45636  dvnprodlem1  45983  dvnprodlem2  45984  fourierdlem11  46155  fourierdlem12  46156  fourierdlem13  46157  fourierdlem14  46158  fourierdlem34  46178  fourierdlem41  46185  fourierdlem48  46191  fourierdlem49  46192  fourierdlem54  46197  fourierdlem63  46206  fourierdlem64  46207  fourierdlem65  46208  fourierdlem69  46212  fourierdlem72  46215  fourierdlem74  46217  fourierdlem75  46218  fourierdlem79  46222  fourierdlem85  46228  fourierdlem88  46231  fourierdlem89  46232  fourierdlem90  46233  fourierdlem91  46234  fourierdlem92  46235  fourierdlem94  46237  fourierdlem97  46240  fourierdlem103  46246  fourierdlem104  46247  fourierdlem111  46254  fourierdlem113  46256  etransclem24  46295  etransclem26  46297  etransclem27  46298  etransclem28  46299  etransclem31  46302  etransclem32  46303  etransclem33  46304  etransclem34  46305  etransclem35  46306  etransclem37  46308  etransclem38  46309  rrxtopnfi  46324  rrndistlt  46327  qndenserrnbllem  46331  rrxsnicc  46337  ioorrnopnlem  46341  subsaliuncl  46395  hoicvr  46585  ovnprodcl  46591  ovnsupge0  46594  ovnlecvr  46595  ovncvrrp  46601  ovn0lem  46602  ovnsubaddlem1  46607  sge0hsphoire  46626  hoidmv1le  46631  hoidmvlelem1  46632  hoidmvlelem2  46633  hoidmvlelem3  46634  hoidmvlelem4  46635  hoidmvlelem5  46636  hoidmvle  46637  ovnhoilem2  46639  ovnlecvr2  46647  ovncvr2  46648  hoiqssbllem1  46659  hoiqssbllem2  46660  hoiqssbllem3  46661  hspmbllem2  46664  opnvonmbllem2  46670  ovolval2lem  46680  ovolval2  46681  ovolval3  46684  ovolval4lem2  46687  ovolval5lem3  46691  ovnovollem1  46693  ovnovollem2  46694  vonvolmbllem  46697  vonvolmbl2  46700  vonvol2  46701  snvonmbl  46723  vonsn  46728  iccpartxr  47449  nnsum4primeseven  47830  nnsum4primesevenALTV  47831  intop  48233  assintop  48239  isassintop  48240  ofaddmndmap  48373  rmsupp0  48398  domnmsuppn0  48399  rmsuppss  48400  scmsuppss  48401  gsumlsscl  48410  lincfsuppcl  48444  linccl  48445  lcosn0  48451  lincdifsn  48455  lincsum  48460  lincscm  48461  lincscmcl  48463  islinindfis  48480  lincext1  48485  lincext2  48486  lincext3  48487  lindslinindimp2lem1  48489  lindslinindimp2lem2  48490  lindslinindimp2lem4  48492  lindslinindsimp2lem5  48493  snlindsntor  48502  lincresunitlem2  48507  lincresunit3lem1  48510  lincresunit3lem2  48511  lincresunit3  48512  lincreslvec3  48513  isldepslvec2  48516  zlmodzxzldeplem2  48532  zlmodzxzldeplem3  48533  ldepsnlinclem1  48536  ldepsnlinclem2  48537  1arymaptf1  48673  1arymaptfo  48674  2arympt  48680  2arymaptf1  48684  2arymaptfo  48685  prelrrx2b  48745  eenglngeehlnmlem1  48768  eenglngeehlnmlem2  48769  aacllem  49832