Theorem elmap 7886

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

Step	Hyp	Ref	Expression
1		elmap.1	. 2 |- A e. _V
2		elmap.2	. 2 |- B e. _V
3		elmapg 7870	. 2 |- ( ( A e. _V /\ B e. _V ) -> ( F e. ( A ^m B ) <-> F : B --> A ) )
4	1, 2, 3	mp2an 708	1 |- ( F e. ( A ^m B ) <-> F : B --> A )

Syntax hints:   <-> wb 196   e. wcel 1990   _Vcvv 3200   -->wf 5884  (class class class)co 6650   ^m cmap 7857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-map 7859

This theorem is referenced by:  mapval2  7887  fvmptmap  7894  mapsn  7899  mapsnconst  7903  mapsncnv  7904  xpmapenlem  8127  pwfseqlem3  9482  tskcard  9603  ingru  9637  rpnnen1lem1  11815  rpnnen1lem3  11816  rpnnen1lem4  11817  rpnnen1lem5  11818  rpnnen1lem1OLD  11821  rpnnen1lem3OLD  11822  rpnnen1lem4OLD  11823  rpnnen1lem5OLD  11824  facmapnn  13072  prmreclem2  15621  1arith  15631  vdwlem6  15690  vdwlem7  15691  vdwlem8  15692  vdwlem9  15693  vdwlem11  15695  vdwlem13  15697  prmgapprmo  15766  isfunc  16524  isfuncd  16525  idfucl  16541  cofucl  16548  funcres2b  16557  wunfunc  16559  catcfuccl  16759  funcestrcsetclem9  16788  ismhm  17337  symgval  17799  dfrhm2  18717  isabv  18819  psrelbas  19379  psraddcl  19383  psrmulcllem  19387  psrvscacl  19393  psr0cl  19394  psrnegcl  19396  psr1cl  19402  subrgpsr  19419  mvrf  19424  mplmon  19463  mplcoe1  19465  coe1fval3  19578  00ply1bas  19610  ply1plusgfvi  19612  coe1z  19633  coe1mul2  19639  coe1tm  19643  pjdm  20051  pjfval2  20053  pnrmopn  21147  distgp  21903  indistgp  21904  elovolm  23243  elovolmr  23244  ovolmge0  23245  ovolgelb  23248  ovolunlem1a  23264  ovolunlem1  23265  ovoliunlem1  23270  ovoliunlem2  23271  ovolshftlem2  23278  ovolicc2  23290  ioombl1  23330  itg2seq  23509  coeeulem  23980  coeeq  23983  aannenlem1  24083  dvntaylp  24125  taylthlem1  24127  taylthlem2  24128  pserdvlem2  24182  lgamgulmlem6  24760  sqff1o  24908  isismt  25429  elee  25774  islno  27608  nmooval  27618  ajfval  27664  h2hcau  27836  h2hlm  27837  hcau  28041  hlimadd  28050  hhcms  28060  hlim0  28092  hhsscms  28136  pjmf1  28575  hosmval  28594  hommval  28595  hodmval  28596  hfsmval  28597  hfmmval  28598  elcnop  28716  ellnop  28717  elhmop  28732  hmopex  28734  nlfnval  28740  elcnfn  28741  ellnfn  28742  dmadjss  28746  dmadjop  28747  adjeu  28748  adjval  28749  hhcno  28763  hhcnf  28764  adjbdln  28942  isst  29072  ishst  29073  maprnin  29506  fpwrelmap  29508  fpwrelmapffs  29509  eulerpartleme  30425  eulerpartlemt  30433  eulerpartlemr  30436  eulerpartlemmf  30437  eulerpartlemgvv  30438  eulerpartlemgs2  30442  eulerpartlemn  30443  reprinfz1  30700  breprexplemb  30709  breprexpnat  30712  vtsval  30715  circlemethnat  30719  circlemethhgt  30721  mrsubff  31409  mrsubrn  31410  msubff  31427  poimirlem3  33412  poimirlem4  33413  poimirlem17  33426  poimirlem20  33429  poimirlem24  33433  poimirlem25  33434  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  isrngohom  33764  islfl  34347  islpolN  36772  constmap  37276  mzpclall  37290  mzpf  37299  mzpindd  37309  mzpcompact2lem  37314  eldiophb  37320  mendring  37762  clsk1independent  38344  k0004lem3  38447  dvnprodlem3  40163  fourierdlem70  40393  fourierdlem102  40425  fourierdlem114  40437  etransclem35  40486  hoicvrrex  40770  ovnhoilem1  40815  ovnovollem2  40871  nnsum3primes4  41676  nnsum3primesprm  41678  ismgmhm  41783  aacllem  42547