Theorem elmap 8819

Description: Membership relation for set exponentiation. (Contributed by NM, 8-Dec-2003.)

Hypotheses

Ref	Expression
elmap.1	⊢ 𝐴 ∈ V
elmap.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
elmap	⊢ (𝐹 ∈ (𝐴 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐴)

Proof of Theorem elmap

Step	Hyp	Ref	Expression
1		elmap.1	. 2 ⊢ 𝐴 ∈ V
2		elmap.2	. 2 ⊢ 𝐵 ∈ V
3		elmapg 8786	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐹 ∈ (𝐴 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐴))
4	1, 2, 3	mp2an 693	1 ⊢ (𝐹 ∈ (𝐴 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐴)

Syntax hints:   ↔ wb 206   ∈ wcel 2114  Vcvv 3429  ⟶wf 6494  (class class class)co 7367   ↑_m cmap 8773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-map 8775

This theorem is referenced by:  mapval2  8820  fvmptmap  8829  mapsnconst  8840  mapsncnv  8841  xpmapenlem  9082  pwfseqlem3  10583  tskcard  10704  ingru  10738  rpnnen1lem1  12928  rpnnen1lem3  12929  rpnnen1lem4  12930  rpnnen1lem5  12931  facmapnn  14247  prmreclem2  16888  1arith  16898  vdwlem6  16957  vdwlem7  16958  vdwlem8  16959  vdwlem9  16960  vdwlem11  16962  vdwlem13  16964  prmgapprmo  17033  isfunc  17831  isfuncd  17832  idfucl  17848  cofucl  17855  funcres2b  17864  wunfunc  17868  catcfuccl  18085  funcestrcsetclem9  18114  ismgmhm  18664  ismhm  18753  efmnd1bas  18861  smndex1ibas  18868  smndex1gbas  18870  smndex1gbasOLD  18871  dfrhm2  20454  isabv  20788  pjdm  21687  pjfval2  21689  psrelbas  21914  psraddcl  21918  psrmulcllem  21924  psrvscacl  21930  psr0cl  21931  psrnegcl  21933  psr1cl  21939  subrgpsr  21956  mvrf  21963  mplmon  22013  mplcoe1  22015  coe1fval3  22172  00ply1bas  22203  ply1plusgfvi  22205  coe1z  22228  coe1mul2  22234  coe1tm  22238  pnrmopn  23308  distgp  24064  indistgp  24065  ehl1eudis  25387  ehl2eudis  25389  elovolmlem  25441  itg2seq  25709  coeeulem  26189  coeeq  26192  aannenlem1  26294  dvntaylp  26336  taylthlem1  26338  taylthlem2  26339  pserdvlem2  26393  lgamgulmlem6  26997  sqff1o  27145  isismt  28602  elee  28962  islno  30824  nmooval  30834  ajfval  30880  h2hcau  31050  h2hlm  31051  hcau  31255  hlimadd  31264  hhcms  31274  hlim0  31306  hhsscms  31349  pjmf1  31787  hosmval  31806  hommval  31807  hodmval  31808  hfsmval  31809  hfmmval  31810  elcnop  31928  ellnop  31929  elhmop  31944  hmopex  31946  nlfnval  31952  elcnfn  31953  ellnfn  31954  dmadjss  31958  dmadjop  31959  adjeu  31960  adjval  31961  hhcno  31975  hhcnf  31976  adjbdln  32154  isst  32284  ishst  32285  maprnin  32804  fpwrelmap  32806  fpwrelmapffs  32807  ismnt  33043  mgcval  33047  fply1  33618  psrmon  33693  zarcmplem  34025  eulerpartleme  34507  eulerpartlemt  34515  eulerpartlemr  34518  eulerpartlemmf  34519  eulerpartlemgvv  34520  eulerpartlemgs2  34524  eulerpartlemn  34525  reprinfz1  34766  breprexplemb  34775  breprexpnat  34778  vtsval  34781  circlemethnat  34785  circlemethhgt  34787  ex-sategoelel12  35609  mrsubff  35694  mrsubrn  35695  msubff  35712  poimirlem3  37944  poimirlem4  37945  poimirlem17  37958  poimirlem20  37961  poimirlem24  37965  poimirlem25  37966  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  isrngohom  38286  islfl  39506  islpolN  41929  constmap  43145  mzpclall  43159  mzpf  43168  mzpindd  43178  mzpcompact2lem  43183  eldiophb  43189  mendring  43616  clsk1independent  44473  k0004lem3  44576  mnringmulrcld  44655  dvnprodlem3  46376  fourierdlem70  46604  fourierdlem102  46636  fourierdlem114  46648  etransclem35  46697  hoicvrrex  46984  ovnhoilem1  47029  ovnovollem2  47085  nnsum3primes4  48264  nnsum3primesprm  48266  grimfn  48355  isgrim  48358  rrx2xpref1o  49194  rrx2linesl  49219  line2  49228  line2x  49230  line2y  49231  funcf2lem  49556  aacllem  50276