Theorem elmap 7505

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 7490	. 2 |- ( ( A e. _V /\ B e. _V ) -> ( F e. ( A ^m B ) <-> F : B --> A ) )
4	1, 2, 3	mp2an 679	1 |- ( F e. ( A ^m B ) <-> F : B --> A )

Syntax hints:   <-> wb 188   e. wcel 1889   _Vcvv 3047   -->wf 5581  (class class class)co 6295   ^m cmap 7477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-sbc 3270  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-fv 5593  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-map 7479

This theorem is referenced by:  mapval2  7506  fvmptmap  7513  mapsn  7518  mapsnconst  7522  mapsncnv  7523  xpmapenlem  7744  pwfseqlem3  9090  tskcard  9211  ingru  9245  rpnnen1lem1  11297  rpnnen1lem3  11299  rpnnen1lem4  11300  rpnnen1lem5  11301  facmapnn  12477  prmreclem2  14873  1arith  14883  vdwlem6  14948  vdwlem7  14949  vdwlem8  14950  vdwlem9  14951  vdwlem11  14953  vdwlem13  14955  lcmsmapnnOLD  15023  prmormapnnOLD  15026  prmgapprmo  15045  isfunc  15781  isfuncd  15782  idfucl  15798  cofucl  15805  funcres2b  15814  wunfunc  15816  catcfuccl  16016  funcestrcsetclem9  16045  ismhm  16596  symgval  17032  dfrhm2  17957  isabv  18059  psrelbas  18615  psraddcl  18619  psrmulcllem  18623  psrvscacl  18629  psr0cl  18630  psrnegcl  18632  psr1cl  18638  subrgpsr  18655  mvrf  18660  mplmon  18699  mplcoe1  18701  coe1fval3  18813  00ply1bas  18845  ply1plusgfvi  18847  coe1z  18868  coe1mul2  18874  coe1tm  18878  pjdm  19282  pjfval2  19284  pnrmopn  20371  distgp  21126  indistgp  21127  elovolm  22440  elovolmr  22441  ovolmge0  22442  ovolgelb  22445  ovolunlem1a  22461  ovolunlem1  22462  ovoliunlem1  22467  ovoliunlem2  22468  ovolshftlem2  22475  ovolicc2  22488  ioombl1  22527  itg2seq  22712  coeeulem  23190  coeeq  23193  aannenlem1  23296  dvntaylp  23338  taylthlem1  23340  taylthlem2  23341  pserdvlem2  23395  lgamgulmlem6  23971  sqff1o  24121  isismt  24591  elee  24936  islno  26406  nmooval  26416  ajfval  26462  h2hcau  26644  h2hlm  26645  hcau  26849  hlimadd  26858  hhcms  26868  hlim0  26900  hhsscms  26942  pjmf1  27381  hosmval  27400  hommval  27401  hodmval  27402  hfsmval  27403  hfmmval  27404  elcnop  27522  ellnop  27523  elhmop  27538  hmopex  27540  nlfnval  27546  elcnfn  27547  ellnfn  27548  dmadjss  27552  dmadjop  27553  adjeu  27554  adjval  27555  hhcno  27569  hhcnf  27570  adjbdln  27748  isst  27878  ishst  27879  maprnin  28328  fpwrelmap  28330  fpwrelmapffs  28331  eulerpartleme  29208  eulerpartlemt  29216  eulerpartlemr  29219  eulerpartlemmf  29220  eulerpartlemgvv  29221  eulerpartlemgs2  29225  eulerpartlemn  29226  mrsubff  30162  mrsubrn  30163  msubff  30180  poimirlem3  31955  poimirlem4  31956  poimirlem17  31969  poimirlem20  31972  poimirlem24  31976  poimirlem25  31977  poimirlem29  31981  poimirlem30  31982  poimirlem31  31983  poimirlem32  31984  isrngohom  32216  islfl  32638  islpolN  35063  constmap  35567  mzpclall  35581  mzpf  35590  mzpindd  35600  mzpcompact2lem  35605  eldiophb  35611  mendring  36070  dvnprodlem3  37833  fourierdlem70  38050  fourierdlem102  38082  fourierdlem114  38094  etransclem35  38144  hoicvrrex  38388  ovnhoilem1  38433  nnsum3primes4  38893  nnsum3primesprm  38895  ismgmhm  39887  aacllem  40644