Theorem elmap 8883

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 8843	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐹 ∈ (𝐴 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐴))
4	1, 2, 3	mp2an 705	1 ⊢ (𝐹 ∈ (𝐴 ↑m 𝐵) ↔ 𝐹:𝐵⟶𝐴)

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  Vcvv 3451  ⟶wf 6527  (class class class)co 7412   ↑_m cmap 8831

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417  df-map 8833

This theorem is used by:  mapval2  8884  fvmptmap  8893  mapsnconst  8904  mapsncnv  8905  xpmapenlem  9147  pwfseqlem3  10726  tskcard  10847  ingru  10881  rpnnen1lem1  13087  rpnnen1lem3  13088  rpnnen1lem4  13089  rpnnen1lem5  13090  facmapnn  14409  prmreclem2  17075  1arith  17085  vdwlem6  17144  vdwlem7  17145  vdwlem8  17146  vdwlem9  17147  vdwlem11  17149  vdwlem13  17151  prmgapprmo  17220  isfunc  18019  isfuncd  18020  idfucl  18036  cofucl  18043  funcres2b  18052  wunfunc  18056  catcfuccl  18273  funcestrcsetclem9  18302  ismgmhm  18865  ismhm  18960  efmnd1bas  19069  smndex1ibas  19076  smndex1gbas  19078  smndex1gbasOLD  19079  dfrhm2  20684  isrhm0  20686  isabv  21048  pjdm  21993  pjfval2  21995  psrelbas  22223  psraddcl  22227  psrmulcllem  22233  psrvscacl  22239  psr0cl  22240  psrnegcl  22242  psr1cl  22248  subrgpsr  22265  mvrf  22272  mplmon  22324  mplcoe1  22326  coe1fval3  22506  00ply1bas  22537  ply1plusgfvi  22539  coe1z  22562  coe1mul2  22568  coe1tm  22572  pnrmopn  23641  distgp  24398  indistgp  24399  ehl1eudis  25721  ehl2eudis  25723  elovolmlem  25775  itg2seq  26043  coeeulem  26523  coeeq  26526  aannenlem1  26637  dvntaylp  26680  taylthlem1  26682  taylthlem2  26683  pserdvlem2  26737  lgamgulmlem6  27343  sqff1o  27491  isismt  28979  elee  29453  islno  31337  nmooval  31347  ajfval  31393  h2hcau  31563  h2hlm  31564  hcau  31768  hlimadd  31777  hhcms  31787  hlim0  31819  hhsscms  31862  pjmf1  32300  hosmval  32319  hommval  32320  hodmval  32321  hfsmval  32322  hfmmval  32323  elcnop  32441  ellnop  32442  elhmop  32457  hmopex  32459  nlfnval  32465  elcnfn  32466  ellnfn  32467  dmadjss  32471  dmadjop  32472  adjeu  32473  adjval  32474  hhcno  32488  hhcnf  32489  adjbdln  32667  isst  32797  ishst  32798  maprnin  33305  fpwrelmap  33307  fpwrelmapffs  33308  ismnt  33526  mgcval  33530  fply1  34072  psrmon  34163  zarcmplem  34495  eulerpartleme  34978  eulerpartlemt  34986  eulerpartlemr  34989  eulerpartlemmf  34990  eulerpartlemgvv  34991  eulerpartlemgs2  34995  eulerpartlemn  34996  reprinfz1  35234  breprexplemb  35243  breprexpnat  35246  vtsval  35249  circlemethnat  35253  circlemethhgt  35255  ex-sategoelel12  36161  mrsubff  36246  mrsubrn  36247  msubff  36264  poimirlem3  38509  poimirlem4  38510  poimirlem17  38523  poimirlem20  38526  poimirlem24  38530  poimirlem25  38531  poimirlem29  38535  poimirlem30  38536  poimirlem31  38537  poimirlem32  38538  isrngohom  38867  islfl  40085  islpolN  42508  constmap  43677  mzpclall  43691  mzpf  43700  mzpindd  43710  mzpcompact2lem  43715  eldiophb  43721  mendring  44148  clsk1independent  45005  k0004lem3  45108  mnringmulrcld  45185  dvnprodlem3  46902  fourierdlem70  47130  fourierdlem102  47162  fourierdlem114  47174  etransclem35  47223  hoicvrrex  47510  ovnhoilem1  47555  ovnovollem2  47611  nnsum3primes4  48830  nnsum3primesprm  48832  grimfn  48921  isgrim  48924  rrx2xpref1o  49774  rrx2linesl  49799  line2  49808  line2x  49810  line2y  49811  funcf2lem  50133  aacllem  50883  crosspcld  50903  veronesematbasd  50924  veroquadmodzerod  50928  veroquadnolindfd  50929  veroquaddetzerod  50930