Theorem elmap 8883

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  Vcvv 3459  ⟶wf 6526  (class class class)co 7403   ↑_m cmap 8838

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 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-fv 6538  df-ov 7406  df-oprab 7407  df-mpo 7408  df-map 8840

This theorem is referenced by:  mapval2  8884  fvmptmap  8893  mapsnconst  8904  mapsncnv  8905  xpmapenlem  9156  pwfseqlem3  10672  tskcard  10793  ingru  10827  rpnnen1lem1  12992  rpnnen1lem3  12993  rpnnen1lem4  12994  rpnnen1lem5  12995  facmapnn  14301  prmreclem2  16935  1arith  16945  vdwlem6  17004  vdwlem7  17005  vdwlem8  17006  vdwlem9  17007  vdwlem11  17009  vdwlem13  17011  prmgapprmo  17080  isfunc  17875  isfuncd  17876  idfucl  17892  cofucl  17899  funcres2b  17908  wunfunc  17912  catcfuccl  18129  funcestrcsetclem9  18158  ismgmhm  18672  ismhm  18761  efmnd1bas  18869  smndex1ibas  18876  smndex1gbas  18878  dfrhm2  20432  isabv  20769  pjdm  21665  pjfval2  21667  psrelbas  21892  psraddcl  21896  psraddclOLD  21897  psrmulcllem  21903  psrvscacl  21909  psr0cl  21910  psrnegcl  21912  psr1cl  21919  subrgpsr  21936  mvrf  21943  mplmon  21991  mplcoe1  21993  coe1fval3  22142  00ply1bas  22173  ply1plusgfvi  22175  coe1z  22198  coe1mul2  22204  coe1tm  22208  pnrmopn  23279  distgp  24035  indistgp  24036  ehl1eudis  25370  ehl2eudis  25372  elovolmlem  25425  itg2seq  25693  coeeulem  26179  coeeq  26182  aannenlem1  26286  dvntaylp  26329  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  pserdvlem2  26388  lgamgulmlem6  26994  sqff1o  27142  isismt  28459  elee  28819  islno  30680  nmooval  30690  ajfval  30736  h2hcau  30906  h2hlm  30907  hcau  31111  hlimadd  31120  hhcms  31130  hlim0  31162  hhsscms  31205  pjmf1  31643  hosmval  31662  hommval  31663  hodmval  31664  hfsmval  31665  hfmmval  31666  elcnop  31784  ellnop  31785  elhmop  31800  hmopex  31802  nlfnval  31808  elcnfn  31809  ellnfn  31810  dmadjss  31814  dmadjop  31815  adjeu  31816  adjval  31817  hhcno  31831  hhcnf  31832  adjbdln  32010  isst  32140  ishst  32141  maprnin  32654  fpwrelmap  32656  fpwrelmapffs  32657  ismnt  32909  mgcval  32913  fply1  33517  zarcmplem  33858  eulerpartleme  34341  eulerpartlemt  34349  eulerpartlemr  34352  eulerpartlemmf  34353  eulerpartlemgvv  34354  eulerpartlemgs2  34358  eulerpartlemn  34359  reprinfz1  34600  breprexplemb  34609  breprexpnat  34612  vtsval  34615  circlemethnat  34619  circlemethhgt  34621  ex-sategoelel12  35395  mrsubff  35480  mrsubrn  35481  msubff  35498  poimirlem3  37593  poimirlem4  37594  poimirlem17  37607  poimirlem20  37610  poimirlem24  37614  poimirlem25  37615  poimirlem29  37619  poimirlem30  37620  poimirlem31  37621  poimirlem32  37622  isrngohom  37935  islfl  39024  islpolN  41448  constmap  42683  mzpclall  42697  mzpf  42706  mzpindd  42716  mzpcompact2lem  42721  eldiophb  42727  mendring  43159  clsk1independent  44017  k0004lem3  44120  mnringmulrcld  44200  dvnprodlem3  45925  fourierdlem70  46153  fourierdlem102  46185  fourierdlem114  46197  etransclem35  46246  hoicvrrex  46533  ovnhoilem1  46578  ovnovollem2  46634  nnsum3primes4  47750  nnsum3primesprm  47752  grimfn  47840  isgrim  47843  rrx2xpref1o  48646  rrx2linesl  48671  line2  48680  line2x  48682  line2y  48683  funcf2lem  48994  aacllem  49613