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

Theorem elmap 7009
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 6998 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( F  e.  ( A  ^m  B )  <-> 
F : B --> A ) )
41, 2, 3mp2an 654 1  |-  ( F  e.  ( A  ^m  B )  <->  F : B
--> A )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    e. wcel 1721   _Vcvv 2924   -->wf 5417  (class class class)co 6048    ^m cmap 6985
This theorem is referenced by:  mapval2  7010  fvmptmap  7017  mapsn  7022  mapsnconst  7026  mapsncnv  7027  xpmapenlem  7241  pwfseqlem3  8499  tskcard  8620  ingru  8654  rpnnen1lem1  10564  rpnnen1lem3  10566  rpnnen1lem4  10567  rpnnen1lem5  10568  prmreclem2  13248  1arith  13258  vdwlem6  13317  vdwlem7  13318  vdwlem8  13319  vdwlem9  13320  vdwlem11  13322  vdwlem13  13324  isfunc  14024  isfuncd  14025  idfucl  14041  cofucl  14048  funcres2b  14057  wunfunc  14059  catcfuccl  14227  ismhm  14703  symgval  15057  dfrhm2  15784  isabv  15870  psrelbas  16407  psraddcl  16410  psrmulcllem  16414  psrvscacl  16420  psr0cl  16421  psrnegcl  16423  psr1cl  16429  subrgpsr  16445  mvrf  16451  mplmon  16489  mplcoe1  16491  coe1fval3  16569  00ply1bas  16597  ply1plusgfvi  16599  coe1z  16619  coe1mul2  16625  coe1tm  16628  pjdm  16897  pjfval2  16899  pnrmopn  17369  distgp  18090  indistgp  18091  elovolm  19332  elovolmr  19333  ovolmge0  19334  ovolgelb  19337  ovolunlem1a  19353  ovolunlem1  19354  ovoliunlem1  19359  ovoliunlem2  19360  ovolshftlem2  19367  ovolicc2  19379  ioombl1  19417  itg2seq  19595  coeeulem  20104  coeeq  20107  aannenlem1  20206  dvntaylp  20248  taylthlem1  20250  taylthlem2  20251  pserdvlem2  20305  sqff1o  20926  islno  22215  nmooval  22225  ajfval  22271  h2hcau  22443  h2hlm  22444  hcau  22647  hlimadd  22656  hhcms  22666  hlim0  22699  hhsscms  22740  pjmf1  23179  hosmval  23199  hommval  23200  hodmval  23201  hfsmval  23202  hfmmval  23203  elcnop  23321  ellnop  23322  elhmop  23337  hmopex  23339  nlfnval  23345  elcnfn  23346  ellnfn  23347  dmadjss  23351  dmadjop  23352  adjeu  23353  adjval  23354  hhcno  23368  hhcnf  23369  adjbdln  23547  isst  23677  ishst  23678  lgamgulmlem6  24779  elee  25745  isrngohom  26479  constmap  26665  mzpclall  26682  mzpf  26691  mzpindd  26701  mzpcompact2lem  26706  eldiophb  26713  mendrng  27376  islfl  29555  islpolN  31978
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-sbc 3130  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-opab 4235  df-id 4466  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-fv 5429  df-ov 6051  df-oprab 6052  df-mpt2 6053  df-map 6987
  Copyright terms: Public domain W3C validator