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

Theorem elmap 6881
Description: Membership relation for set exponentiation. (Contributed by NM, 8-Dec-2003.)
Hypotheses
Ref Expression
elmap.1  |-  A  e. 
_V
elmap.2  |-  B  e. 
_V
Assertion
Ref Expression
elmap  |-  ( F  e.  ( A  ^m  B )  <->  F : B
--> A )

Proof of Theorem elmap
StepHypRef Expression
1 elmap.1 . 2  |-  A  e. 
_V
2 elmap.2 . 2  |-  B  e. 
_V
3 elmapg 6870 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( F  e.  ( A  ^m  B )  <-> 
F : B --> A ) )
41, 2, 3mp2an 653 1  |-  ( F  e.  ( A  ^m  B )  <->  F : B
--> A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    e. wcel 1710   _Vcvv 2864   -->wf 5330  (class class class)co 5942    ^m cmap 6857
This theorem is referenced by:  mapval2  6882  fvmptmap  6889  mapsn  6894  mapsnconst  6898  mapsncnv  6899  xpmapenlem  7113  pwfseqlem3  8369  tskcard  8490  ingru  8524  rpnnen1lem1  10431  rpnnen1lem3  10433  rpnnen1lem4  10434  rpnnen1lem5  10435  prmreclem2  13055  1arith  13065  vdwlem6  13124  vdwlem7  13125  vdwlem8  13126  vdwlem9  13127  vdwlem11  13129  vdwlem13  13131  isfunc  13831  isfuncd  13832  idfucl  13848  cofucl  13855  funcres2b  13864  wunfunc  13866  catcfuccl  14034  ismhm  14510  symgval  14864  dfrhm2  15591  isabv  15677  psrelbas  16218  psraddcl  16221  psrmulcllem  16225  psrvscacl  16231  psr0cl  16232  psrnegcl  16234  psr1cl  16240  subrgpsr  16256  mvrf  16262  mplmon  16300  mplcoe1  16302  coe1fval3  16382  00ply1bas  16411  ply1plusgfvi  16413  coe1z  16433  coe1mul2  16439  coe1tm  16442  pjdm  16707  pjfval2  16709  pnrmopn  17171  distgp  17878  indistgp  17879  elovolm  18932  elovolmr  18933  ovolmge0  18934  ovolgelb  18937  ovolunlem1a  18953  ovolunlem1  18954  ovoliunlem1  18959  ovoliunlem2  18960  ovolshftlem2  18967  ovolicc2  18979  ioombl1  19017  itg2seq  19195  coeeulem  19704  coeeq  19707  aannenlem1  19806  dvntaylp  19848  taylthlem1  19850  taylthlem2  19851  pserdvlem2  19905  sqff1o  20526  islno  21439  nmooval  21449  ajfval  21495  h2hcau  21667  h2hlm  21668  hcau  21871  hlimadd  21880  hhcms  21890  hlim0  21923  hhsscms  21964  pjmf1  22403  hosmval  22423  hommval  22424  hodmval  22425  hfsmval  22426  hfmmval  22427  elcnop  22545  ellnop  22546  elhmop  22561  hmopex  22563  nlfnval  22569  elcnfn  22570  ellnfn  22571  dmadjss  22575  dmadjop  22576  adjeu  22577  adjval  22578  hhcno  22592  hhcnf  22593  adjbdln  22771  isst  22901  ishst  22902  lgamgulmlem6  24067  elee  25081  isrngohom  25919  constmap  26111  mzpclall  26128  mzpf  26137  mzpindd  26147  mzpcompact2lem  26152  eldiophb  26159  mendrng  26823  islfl  29302  islpolN  31725
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293  ax-un 4591
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3907  df-br 4103  df-opab 4157  df-id 4388  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-iota 5298  df-fun 5336  df-fn 5337  df-f 5338  df-fv 5342  df-ov 5945  df-oprab 5946  df-mpt2 5947  df-map 6859
  Copyright terms: Public domain W3C validator