Theorem elmap 8421

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

Syntax hints:   ↔ wb 208   ∈ wcel 2114  Vcvv 3486  ⟶wf 6337  (class class class)co 7142   ↑_m cmap 8392

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3488  df-sbc 3764  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-op 4560  df-uni 4825  df-br 5053  df-opab 5115  df-id 5446  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-fv 6349  df-ov 7145  df-oprab 7146  df-mpo 7147  df-map 8394

This theorem is referenced by:  mapval2  8422  fvmptmap  8431  mapsnconst  8442  mapsncnv  8443  xpmapenlem  8670  pwfseqlem3  10068  tskcard  10189  ingru  10223  rpnnen1lem1  12364  rpnnen1lem3  12365  rpnnen1lem4  12366  rpnnen1lem5  12367  facmapnn  13635  prmreclem2  16236  1arith  16246  vdwlem6  16305  vdwlem7  16306  vdwlem8  16307  vdwlem9  16308  vdwlem11  16310  vdwlem13  16312  prmgapprmo  16381  isfunc  17117  isfuncd  17118  idfucl  17134  cofucl  17141  funcres2b  17150  wunfunc  17152  catcfuccl  17352  funcestrcsetclem9  17381  ismhm  17941  efmnd1bas  18041  smndex1ibas  18048  smndex1gbas  18050  dfrhm2  19452  isabv  19573  psrelbas  20142  psraddcl  20146  psrmulcllem  20150  psrvscacl  20156  psr0cl  20157  psrnegcl  20159  psr1cl  20165  subrgpsr  20182  mvrf  20187  mplmon  20227  mplcoe1  20229  coe1fval3  20359  00ply1bas  20391  ply1plusgfvi  20393  coe1z  20414  coe1mul2  20420  coe1tm  20424  pjdm  20834  pjfval2  20836  pnrmopn  21934  distgp  22690  indistgp  22691  ehl1eudis  24006  ehl2eudis  24008  elovolmlem  24058  itg2seq  24326  coeeulem  24800  coeeq  24803  aannenlem1  24903  dvntaylp  24945  taylthlem1  24947  taylthlem2  24948  pserdvlem2  25002  lgamgulmlem6  25597  sqff1o  25745  isismt  26306  elee  26666  islno  28514  nmooval  28524  ajfval  28570  h2hcau  28740  h2hlm  28741  hcau  28945  hlimadd  28954  hhcms  28964  hlim0  28996  hhsscms  29039  pjmf1  29477  hosmval  29496  hommval  29497  hodmval  29498  hfsmval  29499  hfmmval  29500  elcnop  29618  ellnop  29619  elhmop  29634  hmopex  29636  nlfnval  29642  elcnfn  29643  ellnfn  29644  dmadjss  29648  dmadjop  29649  adjeu  29650  adjval  29651  hhcno  29665  hhcnf  29666  adjbdln  29844  isst  29974  ishst  29975  maprnin  30453  fpwrelmap  30455  fpwrelmapffs  30456  ismnt  30651  mgcval  30655  fply1  30938  eulerpartleme  31628  eulerpartlemt  31636  eulerpartlemr  31639  eulerpartlemmf  31640  eulerpartlemgvv  31641  eulerpartlemgs2  31645  eulerpartlemn  31646  reprinfz1  31900  breprexplemb  31909  breprexpnat  31912  vtsval  31915  circlemethnat  31919  circlemethhgt  31921  ex-sategoelel12  32681  mrsubff  32766  mrsubrn  32767  msubff  32784  poimirlem3  34929  poimirlem4  34930  poimirlem17  34943  poimirlem20  34946  poimirlem24  34950  poimirlem25  34951  poimirlem29  34955  poimirlem30  34956  poimirlem31  34957  poimirlem32  34958  isrngohom  35275  islfl  36228  islpolN  38651  constmap  39402  mzpclall  39416  mzpf  39425  mzpindd  39435  mzpcompact2lem  39440  eldiophb  39446  mendring  39884  clsk1independent  40486  k0004lem3  40589  dvnprodlem3  42323  fourierdlem70  42551  fourierdlem102  42583  fourierdlem114  42595  etransclem35  42644  hoicvrrex  42928  ovnhoilem1  42973  ovnovollem2  43029  nnsum3primes4  44038  nnsum3primesprm  44040  ismgmhm  44135  rrx2xpref1o  44790  rrx2linesl  44815  line2  44824  line2x  44826  line2y  44827  aacllem  44987