Theorem elmapi 8438

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∈ wcel 2111  Vcvv 3409  ⟶wf 6331  (class class class)co 7150   ↑_m cmap 8416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-fv 6343  df-ov 7153  df-oprab 7154  df-mpo 7155  df-1st 7693  df-2nd 7694  df-map 8418

This theorem is referenced by:  mapfset  8439  elmapfn  8447  elmapfun  8448  elmapssres  8449  mapsspm  8458  mapfvd  8461  elmapresaun  8462  map0b  8465  mapss  8471  mapsncnv  8475  ralxpmap  8478  mapen  8703  mapxpen  8705  mapunen  8708  mapfienlem1  8902  mapfienlem2  8903  mapfienlem3  8904  mapfien  8905  wemaplem2  9044  wemappo  9046  wemapsolem  9047  wemapso  9048  wemapso2lem  9049  wemapwe  9193  iunmapdisj  9483  fseqenlem1  9484  fseqenlem2  9485  numacn  9509  finacn  9510  acndom  9511  acndom2  9514  infpwfien  9522  infmap2  9678  fin23lem40  9811  isf32lem12  9824  isf34lem6  9840  acncc  9900  pwfseqlem3  10120  pwxpndom2  10125  ramval  16399  ramub  16404  ramcl  16420  prmgaplem7  16448  prmgaplem8  16449  imasdsval2  16847  funcf2  17197  funcpropd  17229  funcestrcsetclem8  17463  funcestrcsetclem9  17464  funcsetcestrclem8  17478  funcsetcestrclem9  17479  fsfnn0gsumfsffz  19171  gsummptnn0fzfv  19175  frlmfibas  20527  frlmbas3  20541  frlmipval  20544  frlmphllem  20545  frlmphl  20546  elfilspd  20568  islindf4  20603  psrbagf  20680  mplbas2  20802  ltbwe  20804  psr1baslem  20909  psr1basf  20925  fvcoe1  20931  coe1mul2lem1  20991  ply1coe  21020  mamures  21092  mndvcl  21093  mndvass  21094  mndvlid  21095  mndvrid  21096  grpvlinv  21097  grpvrinv  21098  mhmvlin  21099  mamucl  21101  mamuass  21102  mamudi  21103  mamudir  21104  mamuvs1  21105  mamuvs2  21106  mamulid  21141  mamurid  21142  mattposcl  21153  mattpostpos  21154  tposmap  21157  mamutpos  21158  matgsumcl  21160  mavmulcl  21247  mavmulass  21249  mavmulsolcl  21251  marepvcl  21269  1marepvmarrepid  21275  mdetleib2  21288  mdetf  21295  mdetdiaglem  21298  mdetrlin  21302  mdetrsca  21303  mdetralt  21308  mdetunilem7  21318  mdetunilem9  21320  maducoeval2  21340  madutpos  21342  madugsum  21343  madurid  21344  cramerimplem1  21383  m2pmfzmap  21447  decpmatval  21465  pmatcollpw3lem  21483  pmatcollpw3fi1lem1  21486  pmatcollpw3fi1lem2  21487  pm2mp  21525  chfacfisf  21554  chfacfisfcpmat  21555  chfacfscmulgsum  21560  chfacfpmmulgsum  21564  chfacfpmmulgsum2  21565  cayhamlem1  21566  cpmadugsumlemF  21576  cpmadugsumfi  21577  cayhamlem2  21584  chcoeffeqlem  21585  cayleyhamilton1  21592  pnrmopn  22043  xkoptsub  22354  xkopt  22355  tmdgsum  22795  imasdsf1olem  23075  rrxnm  24091  rrxds  24093  rrxf  24101  rrxmvallem  24104  rrxbasefi  24110  rrxdsfi  24111  ehlbase  24115  ovolscalem2  24214  uniioombl  24289  tdeglem2  24761  plypf1  24908  ulmclm  25081  ulmcaulem  25088  ulmcau  25089  ulmss  25091  ulmbdd  25092  ulmcn  25093  ulmdvlem1  25094  ulmdvlem2  25095  ulmdvlem3  25096  mtest  25098  mtestbdd  25099  mbfulm  25100  iblulm  25101  itgulm  25102  itgulm2  25103  adjval2  29773  fmptco1f1o  30490  fcobijfs  30582  resf1o  30589  fpwrelmap  30592  elrspunidl  31127  fply1  31188  fedgmullem1  31231  fedgmul  31233  extdg1id  31259  smatrcl  31267  mbfmf  31741  elmbfmvol2  31753  eulerpartlemelr  31843  eulerpartlemf  31856  eulerpartlemt  31857  eulerpartgbij  31858  eulerpartlemgu  31863  eulerpartlemgh  31864  eulerpartlemgf  31865  eulerpartlemgs2  31866  reprf  32111  reprsuc  32114  vtsprod  32138  circlemethhgt  32142  tgoldbachgtd  32161  satfv1lem  32840  satfvel  32890  satefvfmla0  32896  satefvfmla1  32903  prv1n  32909  mrsubff1  32992  mrsub0  32994  mrsubf  32995  mrsubccat  32996  mrsubcn  32997  msubrn  33007  msubff  33008  msubf  33010  msubff1  33034  mclsind  33048  uncf  35316  curunc  35319  unccur  35320  matunitlindflem1  35333  matunitlindflem2  35334  poimirlem4  35341  poimirlem5  35342  poimirlem6  35343  poimirlem7  35344  poimirlem8  35345  poimirlem10  35347  poimirlem11  35348  poimirlem12  35349  poimirlem16  35353  poimirlem17  35354  poimirlem18  35355  poimirlem19  35356  poimirlem20  35357  poimirlem21  35358  poimirlem22  35359  poimirlem25  35362  poimirlem26  35363  poimirlem27  35364  poimirlem29  35366  poimirlem30  35367  poimirlem31  35368  poimirlem32  35369  poimir  35370  broucube  35371  mblfinlem3  35376  mblfinlem4  35377  ismblfin  35378  rrnmet  35547  rrndstprj1  35548  rrndstprj2  35549  rrncmslem  35550  rrnequiv  35553  evlsbagval  39780  fsuppind  39784  mhphf  39790  mapco2g  40028  mapfzcons1  40031  mapfzcons2  40033  mzpcompact2lem  40065  eldiophb  40071  elmapresaunres2  40085  eq0rabdioph  40090  rexrabdioph  40108  eldioph4b  40125  diophren  40127  rmydioph  40328  rmxdioph  40330  expdiophlem2  40336  expdioph  40337  pw2f1o2val2  40354  wepwsolem  40359  pwfi2f1o  40413  rfovcnvf1od  41078  rfovcnvfvd  41081  fsovrfovd  41083  fsovcnvlem  41087  ntrk0kbimka  41115  neik0pk1imk0  41123  ntrclsfveq1  41136  ntrclsfveq2  41137  ntrclsfveq  41138  ntrclsss  41139  ntrclsiso  41143  ntrclsk2  41144  ntrclskb  41145  ntrclsk3  41146  ntrclsk13  41147  ntrclsk4  41148  ntrneifv3  41158  ntrneineine0lem  41159  ntrneineine1lem  41160  ntrneifv4  41161  ntrneiel2  41162  ntrneicls00  41165  ntrneicls11  41166  ntrneiiso  41167  ntrneik2  41168  ntrneikb  41170  ntrneixb  41171  ntrneik3  41172  ntrneix3  41173  ntrneik13  41174  ntrneix13  41175  ntrneik4w  41176  ntrneik4  41177  clsneifv3  41186  clsneifv4  41187  neicvgfv  41197  k0004ss2  41228  k0004val0  41230  mnringbasefd  41299  mnugrud  41365  mapss2  42204  difmap  42206  inmap  42208  difmapsn  42211  ssmapsn  42215  mccllem  42605  dvnprodlem1  42954  dvnprodlem2  42955  fourierdlem11  43126  fourierdlem12  43127  fourierdlem13  43128  fourierdlem14  43129  fourierdlem34  43149  fourierdlem41  43156  fourierdlem48  43162  fourierdlem49  43163  fourierdlem54  43168  fourierdlem63  43177  fourierdlem64  43178  fourierdlem65  43179  fourierdlem69  43183  fourierdlem72  43186  fourierdlem74  43188  fourierdlem75  43189  fourierdlem79  43193  fourierdlem85  43199  fourierdlem88  43202  fourierdlem89  43203  fourierdlem90  43204  fourierdlem91  43205  fourierdlem92  43206  fourierdlem94  43208  fourierdlem97  43211  fourierdlem103  43217  fourierdlem104  43218  fourierdlem111  43225  fourierdlem113  43227  etransclem24  43266  etransclem26  43268  etransclem27  43269  etransclem28  43270  etransclem31  43273  etransclem32  43274  etransclem33  43275  etransclem34  43276  etransclem35  43277  etransclem37  43279  etransclem38  43280  rrxtopnfi  43295  rrndistlt  43298  qndenserrnbllem  43302  rrxsnicc  43308  ioorrnopnlem  43312  subsaliuncl  43364  hoicvr  43553  ovnprodcl  43559  ovnsupge0  43562  ovnlecvr  43563  ovncvrrp  43569  ovn0lem  43570  ovnsubaddlem1  43575  sge0hsphoire  43594  hoidmv1le  43599  hoidmvlelem1  43600  hoidmvlelem2  43601  hoidmvlelem3  43602  hoidmvlelem4  43603  hoidmvlelem5  43604  hoidmvle  43605  ovnhoilem2  43607  ovnlecvr2  43615  ovncvr2  43616  hoiqssbllem1  43627  hoiqssbllem2  43628  hoiqssbllem3  43629  hspmbllem2  43632  opnvonmbllem2  43638  ovolval2lem  43648  ovolval2  43649  ovolval3  43652  ovolval4lem2  43655  ovolval5lem3  43659  ovnovollem1  43661  ovnovollem2  43662  vonvolmbllem  43665  vonvolmbl2  43668  vonvol2  43669  snvonmbl  43691  vonsn  43696  iccpartxr  44304  nnsum4primeseven  44685  nnsum4primesevenALTV  44686  intop  44830  assintop  44836  isassintop  44837  ofaddmndmap  45112  rmsupp0  45137  domnmsuppn0  45138  rmsuppss  45139  mndpsuppss  45140  scmsuppss  45141  gsumlsscl  45152  lincfsuppcl  45187  linccl  45188  lcosn0  45194  lincdifsn  45198  lincsum  45203  lincscm  45204  lincscmcl  45206  islinindfis  45223  lincext1  45228  lincext2  45229  lincext3  45230  lindslinindimp2lem1  45232  lindslinindimp2lem2  45233  lindslinindimp2lem4  45235  lindslinindsimp2lem5  45236  snlindsntor  45245  lincresunitlem2  45250  lincresunit3lem1  45253  lincresunit3lem2  45254  lincresunit3  45255  lincreslvec3  45256  isldepslvec2  45259  zlmodzxzldeplem2  45275  zlmodzxzldeplem3  45276  ldepsnlinclem1  45279  ldepsnlinclem2  45280  1arymaptf1  45421  1arymaptfo  45422  2arympt  45428  2arymaptf1  45432  2arymaptfo  45433  prelrrx2b  45493  eenglngeehlnmlem1  45516  eenglngeehlnmlem2  45517  aacllem  45720