Theorem elmap 7366

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

Syntax hints:   <-> wb 184   e. wcel 1826   _Vcvv 3034   -->wf 5492  (class class class)co 6196   ^m cmap 7338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-fv 5504  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-map 7340

This theorem is referenced by:  mapval2  7367  fvmptmap  7374  mapsn  7379  mapsnconst  7383  mapsncnv  7384  xpmapenlem  7603  pwfseqlem3  8949  tskcard  9070  ingru  9104  rpnnen1lem1  11127  rpnnen1lem3  11129  rpnnen1lem4  11130  rpnnen1lem5  11131  prmreclem2  14437  1arith  14447  vdwlem6  14506  vdwlem7  14507  vdwlem8  14508  vdwlem9  14509  vdwlem11  14511  vdwlem13  14513  isfunc  15270  isfuncd  15271  idfucl  15287  cofucl  15294  funcres2b  15303  wunfunc  15305  catcfuccl  15505  funcestrcsetclem9  15534  ismhm  16085  symgval  16521  dfrhm2  17479  isabv  17581  psrelbas  18145  psraddcl  18149  psrmulcllem  18153  psrvscacl  18159  psr0cl  18160  psrnegcl  18162  psr1cl  18168  subrgpsr  18187  mvrf  18193  mplmon  18238  mplcoe1  18240  coe1fval3  18360  00ply1bas  18394  ply1plusgfvi  18396  coe1z  18417  coe1mul2  18423  coe1tm  18427  pjdm  18829  pjfval2  18831  pnrmopn  19930  distgp  20683  indistgp  20684  elovolm  21971  elovolmr  21972  ovolmge0  21973  ovolgelb  21976  ovolunlem1a  21992  ovolunlem1  21993  ovoliunlem1  21998  ovoliunlem2  21999  ovolshftlem2  22006  ovolicc2  22018  ioombl1  22057  itg2seq  22234  coeeulem  22706  coeeq  22709  aannenlem1  22809  dvntaylp  22851  taylthlem1  22853  taylthlem2  22854  pserdvlem2  22908  sqff1o  23573  isismt  24041  elee  24318  islno  25785  nmooval  25795  ajfval  25841  h2hcau  26013  h2hlm  26014  hcau  26218  hlimadd  26227  hhcms  26237  hlim0  26270  hhsscms  26312  pjmf1  26751  hosmval  26770  hommval  26771  hodmval  26772  hfsmval  26773  hfmmval  26774  elcnop  26892  ellnop  26893  elhmop  26908  hmopex  26910  nlfnval  26916  elcnfn  26917  ellnfn  26918  dmadjss  26922  dmadjop  26923  adjeu  26924  adjval  26925  hhcno  26939  hhcnf  26940  adjbdln  27118  isst  27248  ishst  27249  maprnin  27704  fpwrelmap  27706  fpwrelmapffs  27707  eulerpartleme  28485  eulerpartlemt  28493  eulerpartlemr  28496  eulerpartlemmf  28497  eulerpartlemgvv  28498  eulerpartlemgs2  28502  eulerpartlemn  28503  lgamgulmlem6  28765  mrsubff  29061  mrsubrn  29062  msubff  29079  isrngohom  30534  constmap  30811  mzpclall  30825  mzpf  30834  mzpindd  30844  mzpcompact2lem  30849  eldiophb  30855  mendring  31309  dvnprodlem3  31911  fourierdlem70  32125  fourierdlem102  32157  fourierdlem114  32169  etransclem35  32218  ismgmhm  32789  aacllem  33550  islfl  35198  islpolN  37623