Theorem elmap 8438

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

Syntax hints:   ↔ wb 208   ∈ wcel 2113  Vcvv 3497  ⟶wf 6354  (class class class)co 7159   ↑_m cmap 8409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147  df-rab 3150  df-v 3499  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-br 5070  df-opab 5132  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-fv 6366  df-ov 7162  df-oprab 7163  df-mpo 7164  df-map 8411

This theorem is referenced by:  mapval2  8439  fvmptmap  8448  mapsnconst  8459  mapsncnv  8460  xpmapenlem  8687  pwfseqlem3  10085  tskcard  10206  ingru  10240  rpnnen1lem1  12380  rpnnen1lem3  12381  rpnnen1lem4  12382  rpnnen1lem5  12383  facmapnn  13648  prmreclem2  16256  1arith  16266  vdwlem6  16325  vdwlem7  16326  vdwlem8  16327  vdwlem9  16328  vdwlem11  16330  vdwlem13  16332  prmgapprmo  16401  isfunc  17137  isfuncd  17138  idfucl  17154  cofucl  17161  funcres2b  17170  wunfunc  17172  catcfuccl  17372  funcestrcsetclem9  17401  ismhm  17961  efmnd1bas  18061  smndex1ibas  18068  smndex1gbas  18070  dfrhm2  19472  isabv  19593  psrelbas  20162  psraddcl  20166  psrmulcllem  20170  psrvscacl  20176  psr0cl  20177  psrnegcl  20179  psr1cl  20185  subrgpsr  20202  mvrf  20207  mplmon  20247  mplcoe1  20249  coe1fval3  20379  00ply1bas  20411  ply1plusgfvi  20413  coe1z  20434  coe1mul2  20440  coe1tm  20444  pjdm  20854  pjfval2  20856  pnrmopn  21954  distgp  22710  indistgp  22711  ehl1eudis  24026  ehl2eudis  24028  elovolmlem  24078  itg2seq  24346  coeeulem  24817  coeeq  24820  aannenlem1  24920  dvntaylp  24962  taylthlem1  24964  taylthlem2  24965  pserdvlem2  25019  lgamgulmlem6  25614  sqff1o  25762  isismt  26323  elee  26683  islno  28533  nmooval  28543  ajfval  28589  h2hcau  28759  h2hlm  28760  hcau  28964  hlimadd  28973  hhcms  28983  hlim0  29015  hhsscms  29058  pjmf1  29496  hosmval  29515  hommval  29516  hodmval  29517  hfsmval  29518  hfmmval  29519  elcnop  29637  ellnop  29638  elhmop  29653  hmopex  29655  nlfnval  29661  elcnfn  29662  ellnfn  29663  dmadjss  29667  dmadjop  29668  adjeu  29669  adjval  29670  hhcno  29684  hhcnf  29685  adjbdln  29863  isst  29993  ishst  29994  maprnin  30470  fpwrelmap  30472  fpwrelmapffs  30473  fply1  30935  eulerpartleme  31625  eulerpartlemt  31633  eulerpartlemr  31636  eulerpartlemmf  31637  eulerpartlemgvv  31638  eulerpartlemgs2  31642  eulerpartlemn  31643  reprinfz1  31897  breprexplemb  31906  breprexpnat  31909  vtsval  31912  circlemethnat  31916  circlemethhgt  31918  ex-sategoelel12  32678  mrsubff  32763  mrsubrn  32764  msubff  32781  poimirlem3  34899  poimirlem4  34900  poimirlem17  34913  poimirlem20  34916  poimirlem24  34920  poimirlem25  34921  poimirlem29  34925  poimirlem30  34926  poimirlem31  34927  poimirlem32  34928  isrngohom  35247  islfl  36200  islpolN  38623  constmap  39316  mzpclall  39330  mzpf  39339  mzpindd  39349  mzpcompact2lem  39354  eldiophb  39360  mendring  39798  clsk1independent  40402  k0004lem3  40505  dvnprodlem3  42239  fourierdlem70  42468  fourierdlem102  42500  fourierdlem114  42512  etransclem35  42561  hoicvrrex  42845  ovnhoilem1  42890  ovnovollem2  42946  nnsum3primes4  43960  nnsum3primesprm  43962  ismgmhm  44057  rrx2xpref1o  44712  rrx2linesl  44737  line2  44746  line2x  44748  line2y  44749  aacllem  44909