Theorem elmap 7506

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

Syntax hints:   <-> wb 188   e. wcel 1869   _Vcvv 3082   -->wf 5595  (class class class)co 6303   ^m cmap 7478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-sbc 3301  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-opab 4481  df-id 4766  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-fv 5607  df-ov 6306  df-oprab 6307  df-mpt2 6308  df-map 7480

This theorem is referenced by:  mapval2  7507  fvmptmap  7514  mapsn  7519  mapsnconst  7523  mapsncnv  7524  xpmapenlem  7743  pwfseqlem3  9087  tskcard  9208  ingru  9242  rpnnen1lem1  11292  rpnnen1lem3  11294  rpnnen1lem4  11295  rpnnen1lem5  11296  facmapnn  12471  prmreclem2  14854  1arith  14864  vdwlem6  14929  vdwlem7  14930  vdwlem8  14931  vdwlem9  14932  vdwlem11  14934  vdwlem13  14936  lcmsmapnnOLD  15004  prmormapnnOLD  15007  prmgapprmo  15026  isfunc  15762  isfuncd  15763  idfucl  15779  cofucl  15786  funcres2b  15795  wunfunc  15797  catcfuccl  15997  funcestrcsetclem9  16026  ismhm  16577  symgval  17013  dfrhm2  17938  isabv  18040  psrelbas  18596  psraddcl  18600  psrmulcllem  18604  psrvscacl  18610  psr0cl  18611  psrnegcl  18613  psr1cl  18619  subrgpsr  18636  mvrf  18641  mplmon  18680  mplcoe1  18682  coe1fval3  18794  00ply1bas  18826  ply1plusgfvi  18828  coe1z  18849  coe1mul2  18855  coe1tm  18859  pjdm  19262  pjfval2  19264  pnrmopn  20351  distgp  21106  indistgp  21107  elovolm  22420  elovolmr  22421  ovolmge0  22422  ovolgelb  22425  ovolunlem1a  22441  ovolunlem1  22442  ovoliunlem1  22447  ovoliunlem2  22448  ovolshftlem2  22455  ovolicc2  22468  ioombl1  22507  itg2seq  22692  coeeulem  23170  coeeq  23173  aannenlem1  23276  dvntaylp  23318  taylthlem1  23320  taylthlem2  23321  pserdvlem2  23375  lgamgulmlem6  23951  sqff1o  24101  isismt  24571  elee  24916  islno  26386  nmooval  26396  ajfval  26442  h2hcau  26624  h2hlm  26625  hcau  26829  hlimadd  26838  hhcms  26848  hlim0  26880  hhsscms  26922  pjmf1  27361  hosmval  27380  hommval  27381  hodmval  27382  hfsmval  27383  hfmmval  27384  elcnop  27502  ellnop  27503  elhmop  27518  hmopex  27520  nlfnval  27526  elcnfn  27527  ellnfn  27528  dmadjss  27532  dmadjop  27533  adjeu  27534  adjval  27535  hhcno  27549  hhcnf  27550  adjbdln  27728  isst  27858  ishst  27859  maprnin  28316  fpwrelmap  28318  fpwrelmapffs  28319  eulerpartleme  29198  eulerpartlemt  29206  eulerpartlemr  29209  eulerpartlemmf  29210  eulerpartlemgvv  29211  eulerpartlemgs2  29215  eulerpartlemn  29216  mrsubff  30152  mrsubrn  30153  msubff  30170  poimirlem3  31901  poimirlem4  31902  poimirlem17  31915  poimirlem20  31918  poimirlem24  31922  poimirlem25  31923  poimirlem29  31927  poimirlem30  31928  poimirlem31  31929  poimirlem32  31930  isrngohom  32162  islfl  32589  islpolN  35014  constmap  35518  mzpclall  35532  mzpf  35541  mzpindd  35551  mzpcompact2lem  35556  eldiophb  35562  mendring  36022  dvnprodlem3  37687  fourierdlem70  37904  fourierdlem102  37936  fourierdlem114  37948  etransclem35  37998  hoicvrrex  38197  nnsum3primes4  38639  nnsum3primesprm  38641  ismgmhm  39125  aacllem  39884