MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elmapi Structured version   Visualization version   GIF version

Theorem elmapi 8423
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
StepHypRef Expression
1 elmapex 8422 . . 3 (𝐴 ∈ (𝐵m 𝐶) → (𝐵 ∈ V ∧ 𝐶 ∈ V))
2 elmapg 8414 . . 3 ((𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝐴 ∈ (𝐵m 𝐶) ↔ 𝐴:𝐶𝐵))
31, 2syl 17 . 2 (𝐴 ∈ (𝐵m 𝐶) → (𝐴 ∈ (𝐵m 𝐶) ↔ 𝐴:𝐶𝐵))
43ibi 268 1 (𝐴 ∈ (𝐵m 𝐶) → 𝐴:𝐶𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wcel 2107  Vcvv 3500  wf 6350  (class class class)co 7150  m cmap 8401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-fv 6362  df-ov 7153  df-oprab 7154  df-mpo 7155  df-1st 7685  df-2nd 7686  df-map 8403
This theorem is referenced by:  elmapfn  8424  elmapfun  8425  elmapssres  8426  mapsspm  8435  mapfvd  8438  elmapresaun  8439  map0b  8442  mapss  8447  mapsncnv  8451  ralxpmap  8454  mapen  8675  mapxpen  8677  mapunen  8680  mapfienlem1  8862  mapfienlem2  8863  mapfienlem3  8864  mapfien  8865  wemaplem2  9005  wemappo  9007  wemapsolem  9008  wemapso  9009  wemapso2lem  9010  wemapwe  9154  iunmapdisj  9443  fseqenlem1  9444  fseqenlem2  9445  numacn  9469  finacn  9470  acndom  9471  acndom2  9474  infpwfien  9482  infmap2  9634  fin23lem40  9767  isf32lem12  9780  isf34lem6  9796  acncc  9856  pwfseqlem3  10076  pwxpndom2  10081  ramval  16339  ramub  16344  ramcl  16360  prmgaplem7  16388  prmgaplem8  16389  imasdsval2  16784  funcf2  17133  funcpropd  17165  funcestrcsetclem8  17392  funcestrcsetclem9  17393  funcsetcestrclem8  17407  funcsetcestrclem9  17408  fsfnn0gsumfsffz  19039  gsummptnn0fzfv  19043  mplbas2  20186  ltbwe  20188  psr1baslem  20288  psr1basf  20304  fvcoe1  20310  coe1mul2lem1  20370  ply1coe  20399  frlmfibas  20841  frlmbas3  20855  frlmipval  20858  frlmphllem  20859  frlmphl  20860  elfilspd  20882  islindf4  20917  mamures  20936  mndvcl  20937  mndvass  20938  mndvlid  20939  mndvrid  20940  grpvlinv  20941  grpvrinv  20942  mhmvlin  20943  mamucl  20945  mamuass  20946  mamudi  20947  mamudir  20948  mamuvs1  20949  mamuvs2  20950  mamulid  20985  mamurid  20986  mattposcl  20997  mattpostpos  20998  tposmap  21001  mamutpos  21002  matgsumcl  21004  mavmulcl  21091  mavmulass  21093  mavmulsolcl  21095  marepvcl  21113  1marepvmarrepid  21119  mdetleib2  21132  mdetf  21139  mdetdiaglem  21142  mdetrlin  21146  mdetrsca  21147  mdetralt  21152  mdetunilem7  21162  mdetunilem9  21164  maducoeval2  21184  madutpos  21186  madugsum  21187  madurid  21188  cramerimplem1  21227  m2pmfzmap  21290  decpmatval  21308  pmatcollpw3lem  21326  pmatcollpw3fi1lem1  21329  pmatcollpw3fi1lem2  21330  pm2mp  21368  chfacfisf  21397  chfacfisfcpmat  21398  chfacfscmulgsum  21403  chfacfpmmulgsum  21407  chfacfpmmulgsum2  21408  cayhamlem1  21409  cpmadugsumlemF  21419  cpmadugsumfi  21420  cayhamlem2  21427  chcoeffeqlem  21428  cayleyhamilton1  21435  pnrmopn  21886  xkoptsub  22197  xkopt  22198  tmdgsum  22638  imasdsf1olem  22917  rrxnm  23928  rrxds  23930  rrxf  23938  rrxmvallem  23941  rrxbasefi  23947  rrxdsfi  23948  ehlbase  23952  ovolscalem2  24049  uniioombl  24124  tdeglem2  24589  plypf1  24736  ulmclm  24909  ulmcaulem  24916  ulmcau  24917  ulmss  24919  ulmbdd  24920  ulmcn  24921  ulmdvlem1  24922  ulmdvlem2  24923  ulmdvlem3  24924  mtest  24926  mtestbdd  24927  mbfulm  24928  iblulm  24929  itgulm  24930  itgulm2  24931  adjval2  29601  fmptco1f1o  30312  fcobijfs  30391  resf1o  30398  fpwrelmap  30401  fply1  30864  fedgmullem1  30930  fedgmul  30932  extdg1id  30958  smatrcl  30966  mbfmf  31418  elmbfmvol2  31430  eulerpartlemelr  31520  eulerpartlemf  31533  eulerpartlemt  31534  eulerpartgbij  31535  eulerpartlemgu  31540  eulerpartlemgh  31541  eulerpartlemgf  31542  eulerpartlemgs2  31543  reprf  31788  reprsuc  31791  vtsprod  31815  circlemethhgt  31819  tgoldbachgtd  31838  satfv1lem  32512  satfvel  32562  satefvfmla0  32568  satefvfmla1  32575  prv1n  32581  mrsubff1  32664  mrsub0  32666  mrsubf  32667  mrsubccat  32668  mrsubcn  32669  msubrn  32679  msubff  32680  msubf  32682  msubff1  32706  mclsind  32720  uncf  34757  curunc  34760  unccur  34761  matunitlindflem1  34774  matunitlindflem2  34775  poimirlem4  34782  poimirlem5  34783  poimirlem6  34784  poimirlem7  34785  poimirlem8  34786  poimirlem10  34788  poimirlem11  34789  poimirlem12  34790  poimirlem16  34794  poimirlem17  34795  poimirlem18  34796  poimirlem19  34797  poimirlem20  34798  poimirlem21  34799  poimirlem22  34800  poimirlem25  34803  poimirlem26  34804  poimirlem27  34805  poimirlem29  34807  poimirlem30  34808  poimirlem31  34809  poimirlem32  34810  poimir  34811  broucube  34812  mblfinlem3  34817  mblfinlem4  34818  ismblfin  34819  rrnmet  34994  rrndstprj1  34995  rrndstprj2  34996  rrncmslem  34997  rrnequiv  35000  mapco2g  39195  mapfzcons1  39198  mapfzcons2  39200  mzpcompact2lem  39232  eldiophb  39238  elmapresaunres2  39252  eq0rabdioph  39257  rexrabdioph  39275  eldioph4b  39292  diophren  39294  rmydioph  39495  rmxdioph  39497  expdiophlem2  39503  expdioph  39504  pw2f1o2val2  39521  wepwsolem  39526  pwfi2f1o  39580  rfovcnvf1od  40234  rfovcnvfvd  40237  fsovrfovd  40239  fsovcnvlem  40243  ntrk0kbimka  40273  neik0pk1imk0  40281  ntrclsfveq1  40294  ntrclsfveq2  40295  ntrclsfveq  40296  ntrclsss  40297  ntrclsiso  40301  ntrclsk2  40302  ntrclskb  40303  ntrclsk3  40304  ntrclsk13  40305  ntrclsk4  40306  ntrneifv3  40316  ntrneineine0lem  40317  ntrneineine1lem  40318  ntrneifv4  40319  ntrneiel2  40320  ntrneicls00  40323  ntrneicls11  40324  ntrneiiso  40325  ntrneik2  40326  ntrneikb  40328  ntrneixb  40329  ntrneik3  40330  ntrneix3  40331  ntrneik13  40332  ntrneix13  40333  ntrneik4w  40334  ntrneik4  40335  clsneifv3  40344  clsneifv4  40345  neicvgfv  40355  k0004ss2  40386  k0004val0  40388  mnugrud  40504  mapss2  41352  difmap  41354  inmap  41356  difmapsn  41359  ssmapsn  41363  mccllem  41762  dvnprodlem1  42115  dvnprodlem2  42116  fourierdlem11  42288  fourierdlem12  42289  fourierdlem13  42290  fourierdlem14  42291  fourierdlem34  42311  fourierdlem41  42318  fourierdlem48  42324  fourierdlem49  42325  fourierdlem54  42330  fourierdlem63  42339  fourierdlem64  42340  fourierdlem65  42341  fourierdlem69  42345  fourierdlem72  42348  fourierdlem74  42350  fourierdlem75  42351  fourierdlem79  42355  fourierdlem85  42361  fourierdlem88  42364  fourierdlem89  42365  fourierdlem90  42366  fourierdlem91  42367  fourierdlem92  42368  fourierdlem94  42370  fourierdlem97  42373  fourierdlem103  42379  fourierdlem104  42380  fourierdlem111  42387  fourierdlem113  42389  etransclem24  42428  etransclem26  42430  etransclem27  42431  etransclem28  42432  etransclem31  42435  etransclem32  42436  etransclem33  42437  etransclem34  42438  etransclem35  42439  etransclem37  42441  etransclem38  42442  rrxtopnfi  42457  rrndistlt  42460  qndenserrnbllem  42464  rrxsnicc  42470  ioorrnopnlem  42474  subsaliuncl  42526  hoicvr  42715  ovnprodcl  42721  ovnsupge0  42724  ovnlecvr  42725  ovncvrrp  42731  ovn0lem  42732  ovnsubaddlem1  42737  sge0hsphoire  42756  hoidmv1le  42761  hoidmvlelem1  42762  hoidmvlelem2  42763  hoidmvlelem3  42764  hoidmvlelem4  42765  hoidmvlelem5  42766  hoidmvle  42767  ovnhoilem2  42769  ovnlecvr2  42777  ovncvr2  42778  hoiqssbllem1  42789  hoiqssbllem2  42790  hoiqssbllem3  42791  hspmbllem2  42794  opnvonmbllem2  42800  ovolval2lem  42810  ovolval2  42811  ovolval3  42814  ovolval4lem2  42817  ovolval5lem3  42821  ovnovollem1  42823  ovnovollem2  42824  vonvolmbllem  42827  vonvolmbl2  42830  vonvol2  42831  snvonmbl  42853  vonsn  42858  iccpartxr  43430  nnsum4primeseven  43816  nnsum4primesevenALTV  43817  elefmndbas2  43946  intop  44012  assintop  44018  isassintop  44019  ofaddmndmap  44294  rmsupp0  44318  domnmsuppn0  44319  rmsuppss  44320  mndpsuppss  44321  scmsuppss  44322  gsumlsscl  44333  lincfsuppcl  44370  linccl  44371  lcosn0  44377  lincdifsn  44381  lincsum  44386  lincscm  44387  lincscmcl  44389  islinindfis  44406  lincext1  44411  lincext2  44412  lincext3  44413  lindslinindimp2lem1  44415  lindslinindimp2lem2  44416  lindslinindimp2lem4  44418  lindslinindsimp2lem5  44419  snlindsntor  44428  lincresunitlem2  44433  lincresunit3lem1  44436  lincresunit3lem2  44437  lincresunit3  44438  lincreslvec3  44439  isldepslvec2  44442  zlmodzxzldeplem2  44458  zlmodzxzldeplem3  44459  ldepsnlinclem1  44462  ldepsnlinclem2  44463  prelrrx2b  44603  eenglngeehlnmlem1  44626  eenglngeehlnmlem2  44627  aacllem  44804
  Copyright terms: Public domain W3C validator