Theorem elmap 8911

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  Vcvv 3480  ⟶wf 6557  (class class class)co 7431   ↑_m cmap 8866

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 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-map 8868

This theorem is referenced by:  mapval2  8912  fvmptmap  8921  mapsnconst  8932  mapsncnv  8933  xpmapenlem  9184  pwfseqlem3  10700  tskcard  10821  ingru  10855  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem4  13022  rpnnen1lem5  13023  facmapnn  14324  prmreclem2  16955  1arith  16965  vdwlem6  17024  vdwlem7  17025  vdwlem8  17026  vdwlem9  17027  vdwlem11  17029  vdwlem13  17031  prmgapprmo  17100  isfunc  17909  isfuncd  17910  idfucl  17926  cofucl  17933  funcres2b  17942  wunfunc  17946  catcfuccl  18163  funcestrcsetclem9  18193  ismgmhm  18709  ismhm  18798  efmnd1bas  18906  smndex1ibas  18913  smndex1gbas  18915  dfrhm2  20474  isabv  20812  pjdm  21727  pjfval2  21729  psrelbas  21954  psraddcl  21958  psraddclOLD  21959  psrmulcllem  21965  psrvscacl  21971  psr0cl  21972  psrnegcl  21974  psr1cl  21981  subrgpsr  21998  mvrf  22005  mplmon  22053  mplcoe1  22055  coe1fval3  22210  00ply1bas  22241  ply1plusgfvi  22243  coe1z  22266  coe1mul2  22272  coe1tm  22276  pnrmopn  23351  distgp  24107  indistgp  24108  ehl1eudis  25454  ehl2eudis  25456  elovolmlem  25509  itg2seq  25777  coeeulem  26263  coeeq  26266  aannenlem1  26370  dvntaylp  26413  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  pserdvlem2  26472  lgamgulmlem6  27077  sqff1o  27225  isismt  28542  elee  28909  islno  30772  nmooval  30782  ajfval  30828  h2hcau  30998  h2hlm  30999  hcau  31203  hlimadd  31212  hhcms  31222  hlim0  31254  hhsscms  31297  pjmf1  31735  hosmval  31754  hommval  31755  hodmval  31756  hfsmval  31757  hfmmval  31758  elcnop  31876  ellnop  31877  elhmop  31892  hmopex  31894  nlfnval  31900  elcnfn  31901  ellnfn  31902  dmadjss  31906  dmadjop  31907  adjeu  31908  adjval  31909  hhcno  31923  hhcnf  31924  adjbdln  32102  isst  32232  ishst  32233  maprnin  32742  fpwrelmap  32744  fpwrelmapffs  32745  ismnt  32973  mgcval  32977  fply1  33584  zarcmplem  33880  eulerpartleme  34365  eulerpartlemt  34373  eulerpartlemr  34376  eulerpartlemmf  34377  eulerpartlemgvv  34378  eulerpartlemgs2  34382  eulerpartlemn  34383  reprinfz1  34637  breprexplemb  34646  breprexpnat  34649  vtsval  34652  circlemethnat  34656  circlemethhgt  34658  ex-sategoelel12  35432  mrsubff  35517  mrsubrn  35518  msubff  35535  poimirlem3  37630  poimirlem4  37631  poimirlem17  37644  poimirlem20  37647  poimirlem24  37651  poimirlem25  37652  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  isrngohom  37972  islfl  39061  islpolN  41485  constmap  42724  mzpclall  42738  mzpf  42747  mzpindd  42757  mzpcompact2lem  42762  eldiophb  42768  mendring  43200  clsk1independent  44059  k0004lem3  44162  mnringmulrcld  44247  dvnprodlem3  45963  fourierdlem70  46191  fourierdlem102  46223  fourierdlem114  46235  etransclem35  46284  hoicvrrex  46571  ovnhoilem1  46616  ovnovollem2  46672  nnsum3primes4  47775  nnsum3primesprm  47777  grimfn  47865  isgrim  47868  rrx2xpref1o  48639  rrx2linesl  48664  line2  48673  line2x  48675  line2y  48676  funcf2lem  48914  aacllem  49320