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

Theorem elmapi 6835
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  |-  ( A  e.  ( B  ^m  C )  ->  A : C --> B )

Proof of Theorem elmapi
StepHypRef Expression
1 elmapex 6834 . . 3  |-  ( A  e.  ( B  ^m  C )  ->  ( B  e.  _V  /\  C  e.  _V ) )
2 elmapg 6828 . . 3  |-  ( ( B  e.  _V  /\  C  e.  _V )  ->  ( A  e.  ( B  ^m  C )  <-> 
A : C --> B ) )
31, 2syl 15 . 2  |-  ( A  e.  ( B  ^m  C )  ->  ( A  e.  ( B  ^m  C )  <->  A : C
--> B ) )
43ibi 232 1  |-  ( A  e.  ( B  ^m  C )  ->  A : C --> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    e. wcel 1701   _Vcvv 2822   -->wf 5288  (class class class)co 5900    ^m cmap 6815
This theorem is referenced by:  mapsspm  6844  map0b  6849  mapss  6853  mapsncnv  6857  mapen  7068  mapxpen  7070  mapunen  7073  wemaplem2  7307  wemappo  7309  wemapso2lem  7310  wemapso  7311  wemapso2  7312  mapfien  7444  wemapwe  7445  iunmapdisj  7695  fseqenlem1  7696  fseqenlem2  7697  numacn  7721  finacn  7722  acndom  7723  acndom2  7726  infpwfien  7734  infmap2  7889  fin23lem40  8022  isf32lem12  8035  isf34lem6  8051  acncc  8111  pwfseqlem3  8327  pwxpndom2  8332  ramval  13102  ramub  13107  ramcl  13123  imasdsval2  13468  funcf2  13791  funcpropd  13823  ltbwe  16263  psr1baslem  16313  psr1basf  16330  fvcoe1  16337  coe1mul2lem1  16393  ply1coe  16417  pnrmopn  17127  xkoptsub  17404  xkopt  17405  tmdgsum  17830  imasdsf1olem  17989  ovolscalem2  18926  uniioombl  18997  tdeglem2  19500  plypf1  19647  ulmclm  19819  ulmcaulem  19824  ulmcau  19825  ulmss  19827  ulmbdd  19828  ulmcn  19829  ulmdvlem1  19830  ulmdvlem2  19831  ulmdvlem3  19832  mtest  19834  mbfulm  19835  iblulm  19836  itgulm  19837  itgulm2  19838  adjval2  22526  mbfmfun  23778  mbfmf  23779  elmbfmvol2  23791  rrnmet  25701  rrndstprj1  25702  rrndstprj2  25703  rrncmslem  25704  rrnequiv  25707  ralxpmap  25909  elmapfun  25937  mapco2g  25938  elmapssres  25940  mapfzcons1  25942  mapfzcons2  25944  mzpcompact2lem  25977  eldiophb  25984  elmapresaun  25998  elmapresaunres2  25999  eq0rabdioph  26004  rexrabdioph  26023  eldioph4b  26042  diophren  26044  rmydioph  26255  rmxdioph  26257  expdiophlem2  26263  expdioph  26264  pw2f1o2val2  26281  wepwsolem  26286  pwfi2f1o  26408  islindf4  26456  mndvcl  26594  mndvass  26595  mndvlid  26596  mndvrid  26597  grpvlinv  26598  grpvrinv  26599  mhmvlin  26600  mamucl  26604  mamulid  26606  mamurid  26607  mamuass  26608  mamudi  26609  mamudir  26610  mamuvs1  26611  mamuvs2  26612  matbas2  26623
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-iun 3944  df-br 4061  df-opab 4115  df-mpt 4116  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-fv 5300  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-1st 6164  df-2nd 6165  df-map 6817
  Copyright terms: Public domain W3C validator