Theorem elmap 7229

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

Syntax hints:   <-> wb 184   e. wcel 1755   _Vcvv 2962   -->wf 5402  (class class class)co 6080   ^m cmap 7202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-fv 5414  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-map 7204

This theorem is referenced by:  mapval2  7230  fvmptmap  7237  mapsn  7242  mapsnconst  7246  mapsncnv  7247  xpmapenlem  7466  pwfseqlem3  8815  tskcard  8936  ingru  8970  rpnnen1lem1  10967  rpnnen1lem3  10969  rpnnen1lem4  10970  rpnnen1lem5  10971  prmreclem2  13961  1arith  13971  vdwlem6  14030  vdwlem7  14031  vdwlem8  14032  vdwlem9  14033  vdwlem11  14035  vdwlem13  14037  isfunc  14757  isfuncd  14758  idfucl  14774  cofucl  14781  funcres2b  14790  wunfunc  14792  catcfuccl  14960  ismhm  15449  symgval  15864  dfrhm2  16742  isabv  16828  psrelbas  17384  psraddcl  17388  psrmulcllem  17392  psrvscacl  17398  psr0cl  17399  psrnegcl  17401  psr1cl  17407  subrgpsr  17425  mvrf  17431  mplmon  17476  mplcoe1  17478  coe1fval3  17563  00ply1bas  17593  ply1plusgfvi  17595  coe1z  17615  coe1mul2  17621  coe1tm  17624  pjdm  17974  pjfval2  17976  pnrmopn  18789  distgp  19512  indistgp  19513  elovolm  20800  elovolmr  20801  ovolmge0  20802  ovolgelb  20805  ovolunlem1a  20821  ovolunlem1  20822  ovoliunlem1  20827  ovoliunlem2  20828  ovolshftlem2  20835  ovolicc2  20847  ioombl1  20885  itg2seq  21062  coeeulem  21577  coeeq  21580  aannenlem1  21679  dvntaylp  21721  taylthlem1  21723  taylthlem2  21724  pserdvlem2  21778  sqff1o  22405  elee  22963  islno  23976  nmooval  23986  ajfval  24032  h2hcau  24204  h2hlm  24205  hcau  24409  hlimadd  24418  hhcms  24428  hlim0  24461  hhsscms  24503  pjmf1  24942  hosmval  24962  hommval  24963  hodmval  24964  hfsmval  24965  hfmmval  24966  elcnop  25084  ellnop  25085  elhmop  25100  hmopex  25102  nlfnval  25108  elcnfn  25109  ellnfn  25110  dmadjss  25114  dmadjop  25115  adjeu  25116  adjval  25117  hhcno  25131  hhcnf  25132  adjbdln  25310  isst  25440  ishst  25441  maprnin  25856  eulerpartleme  26594  eulerpartlemt  26602  eulerpartlemr  26605  eulerpartlemmf  26606  eulerpartlemgvv  26607  eulerpartlemgs2  26611  eulerpartlemn  26612  lgamgulmlem6  26868  isrngohom  28615  constmap  28894  mzpclall  28908  mzpf  28917  mzpindd  28927  mzpcompact2lem  28933  eldiophb  28940  mendrng  29394  dflinc2  30653  islfl  32278  islpolN  34701