Theorem elmap 7350

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

Syntax hints:   <-> wb 184   e. wcel 1758   _Vcvv 3076   -->wf 5521  (class class class)co 6199   ^m cmap 7323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-sbc 3293  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-opab 4458  df-id 4743  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-fv 5533  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-map 7325

This theorem is referenced by:  mapval2  7351  fvmptmap  7358  mapsn  7363  mapsnconst  7367  mapsncnv  7368  xpmapenlem  7587  pwfseqlem3  8937  tskcard  9058  ingru  9092  rpnnen1lem1  11089  rpnnen1lem3  11091  rpnnen1lem4  11092  rpnnen1lem5  11093  prmreclem2  14095  1arith  14105  vdwlem6  14164  vdwlem7  14165  vdwlem8  14166  vdwlem9  14167  vdwlem11  14169  vdwlem13  14171  isfunc  14892  isfuncd  14893  idfucl  14909  cofucl  14916  funcres2b  14925  wunfunc  14927  catcfuccl  15095  ismhm  15584  symgval  16002  dfrhm2  16930  isabv  17026  psrelbas  17572  psraddcl  17576  psrmulcllem  17580  psrvscacl  17586  psr0cl  17587  psrnegcl  17589  psr1cl  17595  subrgpsr  17614  mvrf  17620  mplmon  17665  mplcoe1  17667  coe1fval3  17787  00ply1bas  17817  ply1plusgfvi  17819  coe1z  17839  coe1mul2  17845  coe1tm  17849  pjdm  18256  pjfval2  18258  pnrmopn  19078  distgp  19801  indistgp  19802  elovolm  21089  elovolmr  21090  ovolmge0  21091  ovolgelb  21094  ovolunlem1a  21110  ovolunlem1  21111  ovoliunlem1  21116  ovoliunlem2  21117  ovolshftlem2  21124  ovolicc2  21136  ioombl1  21175  itg2seq  21352  coeeulem  21824  coeeq  21827  aannenlem1  21926  dvntaylp  21968  taylthlem1  21970  taylthlem2  21971  pserdvlem2  22025  sqff1o  22652  elee  23291  islno  24304  nmooval  24314  ajfval  24360  h2hcau  24532  h2hlm  24533  hcau  24737  hlimadd  24746  hhcms  24756  hlim0  24789  hhsscms  24831  pjmf1  25270  hosmval  25290  hommval  25291  hodmval  25292  hfsmval  25293  hfmmval  25294  elcnop  25412  ellnop  25413  elhmop  25428  hmopex  25430  nlfnval  25436  elcnfn  25437  ellnfn  25438  dmadjss  25442  dmadjop  25443  adjeu  25444  adjval  25445  hhcno  25459  hhcnf  25460  adjbdln  25638  isst  25768  ishst  25769  maprnin  26181  eulerpartleme  26889  eulerpartlemt  26897  eulerpartlemr  26900  eulerpartlemmf  26901  eulerpartlemgvv  26902  eulerpartlemgs2  26906  eulerpartlemn  26907  lgamgulmlem6  27163  isrngohom  28918  constmap  29196  mzpclall  29210  mzpf  29219  mzpindd  29229  mzpcompact2lem  29235  eldiophb  29242  mendrng  29696  dflinc2  31062  islfl  33028  islpolN  35451