Theorem elmap 8454

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

Syntax hints:   ↔ wb 209   ∈ wcel 2112  Vcvv 3410  ⟶wf 6332  (class class class)co 7151   ↑_m cmap 8417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-sbc 3698  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-id 5431  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-fv 6344  df-ov 7154  df-oprab 7155  df-mpo 7156  df-map 8419

This theorem is referenced by:  mapval2  8455  fvmptmap  8464  mapsnconst  8475  mapsncnv  8476  xpmapenlem  8707  pwfseqlem3  10121  tskcard  10242  ingru  10276  rpnnen1lem1  12419  rpnnen1lem3  12420  rpnnen1lem4  12421  rpnnen1lem5  12422  facmapnn  13696  prmreclem2  16309  1arith  16319  vdwlem6  16378  vdwlem7  16379  vdwlem8  16380  vdwlem9  16381  vdwlem11  16383  vdwlem13  16385  prmgapprmo  16454  isfunc  17194  isfuncd  17195  idfucl  17211  cofucl  17218  funcres2b  17227  wunfunc  17229  catcfuccl  17436  funcestrcsetclem9  17465  ismhm  18025  efmnd1bas  18125  smndex1ibas  18132  smndex1gbas  18134  dfrhm2  19541  isabv  19659  pjdm  20473  pjfval2  20475  psrelbas  20708  psraddcl  20712  psrmulcllem  20716  psrvscacl  20722  psr0cl  20723  psrnegcl  20725  psr1cl  20731  subrgpsr  20748  mvrf  20753  mplmon  20796  mplcoe1  20798  coe1fval3  20933  00ply1bas  20965  ply1plusgfvi  20967  coe1z  20988  coe1mul2  20994  coe1tm  20998  pnrmopn  22044  distgp  22800  indistgp  22801  ehl1eudis  24121  ehl2eudis  24123  elovolmlem  24175  itg2seq  24443  coeeulem  24921  coeeq  24924  aannenlem1  25024  dvntaylp  25066  taylthlem1  25068  taylthlem2  25069  pserdvlem2  25123  lgamgulmlem6  25719  sqff1o  25867  isismt  26428  elee  26788  islno  28636  nmooval  28646  ajfval  28692  h2hcau  28862  h2hlm  28863  hcau  29067  hlimadd  29076  hhcms  29086  hlim0  29118  hhsscms  29161  pjmf1  29599  hosmval  29618  hommval  29619  hodmval  29620  hfsmval  29621  hfmmval  29622  elcnop  29740  ellnop  29741  elhmop  29756  hmopex  29758  nlfnval  29764  elcnfn  29765  ellnfn  29766  dmadjss  29770  dmadjop  29771  adjeu  29772  adjval  29773  hhcno  29787  hhcnf  29788  adjbdln  29966  isst  30096  ishst  30097  maprnin  30591  fpwrelmap  30593  fpwrelmapffs  30594  ismnt  30788  mgcval  30792  fply1  31189  zarcmplem  31353  eulerpartleme  31850  eulerpartlemt  31858  eulerpartlemr  31861  eulerpartlemmf  31862  eulerpartlemgvv  31863  eulerpartlemgs2  31867  eulerpartlemn  31868  reprinfz1  32122  breprexplemb  32131  breprexpnat  32134  vtsval  32137  circlemethnat  32141  circlemethhgt  32143  ex-sategoelel12  32906  mrsubff  32991  mrsubrn  32992  msubff  33009  poimirlem3  35341  poimirlem4  35342  poimirlem17  35355  poimirlem20  35358  poimirlem24  35362  poimirlem25  35363  poimirlem29  35367  poimirlem30  35368  poimirlem31  35369  poimirlem32  35370  isrngohom  35684  islfl  36637  islpolN  39060  constmap  40028  mzpclall  40042  mzpf  40051  mzpindd  40061  mzpcompact2lem  40066  eldiophb  40072  mendring  40510  clsk1independent  41123  k0004lem3  41226  mnringmulrcld  41310  dvnprodlem3  42957  fourierdlem70  43185  fourierdlem102  43217  fourierdlem114  43229  etransclem35  43278  hoicvrrex  43562  ovnhoilem1  43607  ovnovollem2  43663  nnsum3primes4  44674  nnsum3primesprm  44676  ismgmhm  44771  rrx2xpref1o  45498  rrx2linesl  45523  line2  45532  line2x  45534  line2y  45535  aacllem  45721