Theorem elmap 8801

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

Syntax hints:   ↔ wb 206   ∈ wcel 2113  Vcvv 3437  ⟶wf 6482  (class class class)co 7352   ↑_m cmap 8756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494  df-ov 7355  df-oprab 7356  df-mpo 7357  df-map 8758

This theorem is referenced by:  mapval2  8802  fvmptmap  8811  mapsnconst  8822  mapsncnv  8823  xpmapenlem  9064  pwfseqlem3  10558  tskcard  10679  ingru  10713  rpnnen1lem1  12878  rpnnen1lem3  12879  rpnnen1lem4  12880  rpnnen1lem5  12881  facmapnn  14194  prmreclem2  16831  1arith  16841  vdwlem6  16900  vdwlem7  16901  vdwlem8  16902  vdwlem9  16903  vdwlem11  16905  vdwlem13  16907  prmgapprmo  16976  isfunc  17773  isfuncd  17774  idfucl  17790  cofucl  17797  funcres2b  17806  wunfunc  17810  catcfuccl  18027  funcestrcsetclem9  18056  ismgmhm  18606  ismhm  18695  efmnd1bas  18803  smndex1ibas  18810  smndex1gbas  18812  dfrhm2  20394  isabv  20728  pjdm  21646  pjfval2  21648  psrelbas  21873  psraddcl  21877  psraddclOLD  21878  psrmulcllem  21884  psrvscacl  21890  psr0cl  21891  psrnegcl  21893  psr1cl  21899  subrgpsr  21916  mvrf  21923  mplmon  21971  mplcoe1  21973  coe1fval3  22122  00ply1bas  22153  ply1plusgfvi  22155  coe1z  22178  coe1mul2  22184  coe1tm  22188  pnrmopn  23259  distgp  24015  indistgp  24016  ehl1eudis  25348  ehl2eudis  25350  elovolmlem  25403  itg2seq  25671  coeeulem  26157  coeeq  26160  aannenlem1  26264  dvntaylp  26307  taylthlem1  26309  taylthlem2  26310  taylthlem2OLD  26311  pserdvlem2  26366  lgamgulmlem6  26972  sqff1o  27120  isismt  28513  elee  28873  islno  30735  nmooval  30745  ajfval  30791  h2hcau  30961  h2hlm  30962  hcau  31166  hlimadd  31175  hhcms  31185  hlim0  31217  hhsscms  31260  pjmf1  31698  hosmval  31717  hommval  31718  hodmval  31719  hfsmval  31720  hfmmval  31721  elcnop  31839  ellnop  31840  elhmop  31855  hmopex  31857  nlfnval  31863  elcnfn  31864  ellnfn  31865  dmadjss  31869  dmadjop  31870  adjeu  31871  adjval  31872  hhcno  31886  hhcnf  31887  adjbdln  32065  isst  32195  ishst  32196  maprnin  32718  fpwrelmap  32720  fpwrelmapffs  32721  ismnt  32971  mgcval  32975  fply1  33528  zarcmplem  33915  eulerpartleme  34397  eulerpartlemt  34405  eulerpartlemr  34408  eulerpartlemmf  34409  eulerpartlemgvv  34410  eulerpartlemgs2  34414  eulerpartlemn  34415  reprinfz1  34656  breprexplemb  34665  breprexpnat  34668  vtsval  34671  circlemethnat  34675  circlemethhgt  34677  ex-sategoelel12  35492  mrsubff  35577  mrsubrn  35578  msubff  35595  poimirlem3  37683  poimirlem4  37684  poimirlem17  37697  poimirlem20  37700  poimirlem24  37704  poimirlem25  37705  poimirlem29  37709  poimirlem30  37710  poimirlem31  37711  poimirlem32  37712  isrngohom  38025  islfl  39179  islpolN  41602  constmap  42830  mzpclall  42844  mzpf  42853  mzpindd  42863  mzpcompact2lem  42868  eldiophb  42874  mendring  43305  clsk1independent  44163  k0004lem3  44266  mnringmulrcld  44345  dvnprodlem3  46070  fourierdlem70  46298  fourierdlem102  46330  fourierdlem114  46342  etransclem35  46391  hoicvrrex  46678  ovnhoilem1  46723  ovnovollem2  46779  nnsum3primes4  47912  nnsum3primesprm  47914  grimfn  48003  isgrim  48006  rrx2xpref1o  48843  rrx2linesl  48868  line2  48877  line2x  48879  line2y  48880  funcf2lem  49206  aacllem  49926