Theorem elmap 8870

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

Syntax hints:   ↔ wb 209   ∈ wcel 2143  Vcvv 3455  ⟶wf 6534  (class class class)co 7412   ↑_m cmap 8825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7415  df-oprab 7416  df-mpo 7417  df-map 8827

This theorem is referenced by:  mapval2  8871  fvmptmap  8880  mapsnconst  8891  mapsncnv  8892  xpmapenlem  9133  pwfseqlem3  10646  tskcard  10767  ingru  10801  rpnnen1lem1  13003  rpnnen1lem3  13004  rpnnen1lem4  13005  rpnnen1lem5  13006  facmapnn  14323  prmreclem2  16978  1arith  16988  vdwlem6  17047  vdwlem7  17048  vdwlem8  17049  vdwlem9  17050  vdwlem11  17052  vdwlem13  17054  prmgapprmo  17123  isfunc  17922  isfuncd  17923  idfucl  17939  cofucl  17946  funcres2b  17955  wunfunc  17959  catcfuccl  18176  funcestrcsetclem9  18205  ismgmhm  18755  ismhm  18844  efmnd1bas  18953  smndex1ibas  18960  smndex1gbas  18962  smndex1gbasOLD  18963  dfrhm2  20557  isabv  20895  pjdm  21838  pjfval2  21840  psrelbas  22066  psraddcl  22070  psrmulcllem  22076  psrvscacl  22082  psr0cl  22083  psrnegcl  22085  psr1cl  22091  subrgpsr  22108  mvrf  22115  mplmon  22167  mplcoe1  22169  coe1fval3  22349  00ply1bas  22380  ply1plusgfvi  22382  coe1z  22405  coe1mul2  22411  coe1tm  22415  pnrmopn  23481  distgp  24237  indistgp  24238  ehl1eudis  25560  ehl2eudis  25562  elovolmlem  25614  itg2seq  25882  coeeulem  26362  coeeq  26365  aannenlem1  26470  dvntaylp  26512  taylthlem1  26514  taylthlem2  26515  pserdvlem2  26569  lgamgulmlem6  27176  sqff1o  27324  isismt  28781  elee  29221  islno  31083  nmooval  31093  ajfval  31139  h2hcau  31309  h2hlm  31310  hcau  31514  hlimadd  31523  hhcms  31533  hlim0  31565  hhsscms  31608  pjmf1  32046  hosmval  32065  hommval  32066  hodmval  32067  hfsmval  32068  hfmmval  32069  elcnop  32187  ellnop  32188  elhmop  32203  hmopex  32205  nlfnval  32211  elcnfn  32212  ellnfn  32213  dmadjss  32217  dmadjop  32218  adjeu  32219  adjval  32220  hhcno  32234  hhcnf  32235  adjbdln  32413  isst  32543  ishst  32544  maprnin  33054  fpwrelmap  33056  fpwrelmapffs  33057  ismnt  33281  mgcval  33285  fply1  33826  psrmon  33917  zarcmplem  34249  eulerpartleme  34731  eulerpartlemt  34739  eulerpartlemr  34742  eulerpartlemmf  34743  eulerpartlemgvv  34744  eulerpartlemgs2  34748  eulerpartlemn  34749  reprinfz1  34987  breprexplemb  34996  breprexpnat  34999  vtsval  35002  circlemethnat  35006  circlemethhgt  35008  ex-sategoelel12  35897  mrsubff  35982  mrsubrn  35983  msubff  36000  poimirlem3  38252  poimirlem4  38253  poimirlem17  38266  poimirlem20  38269  poimirlem24  38273  poimirlem25  38274  poimirlem29  38278  poimirlem30  38279  poimirlem31  38280  poimirlem32  38281  isrngohom  38594  islfl  39812  islpolN  42235  constmap  43424  mzpclall  43438  mzpf  43447  mzpindd  43457  mzpcompact2lem  43462  eldiophb  43468  mendring  43895  clsk1independent  44752  k0004lem3  44855  mnringmulrcld  44932  dvnprodlem3  46642  fourierdlem70  46870  fourierdlem102  46902  fourierdlem114  46914  etransclem35  46963  hoicvrrex  47250  ovnhoilem1  47295  ovnovollem2  47351  nnsum3primes4  48530  nnsum3primesprm  48532  grimfn  48621  isgrim  48624  rrx2xpref1o  49475  rrx2linesl  49500  line2  49509  line2x  49511  line2y  49512  funcf2lem  49836  aacllem  50578