Theorem elmapg 8858

Description: Membership relation for set exponentiation. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.)

Assertion

Ref	Expression
elmapg	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Proof of Theorem elmapg

Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mapvalg 8855	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑m 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2812	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7937	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1121	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1118	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6699	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3673	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 278	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∈ wcel 2099  {cab 2703  Vcvv 3463  ⟶wf 6540  (class class class)co 7414   ↑_m cmap 8845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7736

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ral 3052  df-rex 3061  df-rab 3421  df-v 3465  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4907  df-br 5145  df-opab 5207  df-id 5571  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-ov 7417  df-oprab 7418  df-mpo 7419  df-map 8847

This theorem is referenced by:  elmapd  8859  mapdm0  8861  elmapi  8868  elmap  8890  map0g  8903  fdiagfn  8909  ralxpmap  8915  ixpssmap2g  8946  snmapen  9064  pw2f1olem  9104  mapxpen  9171  fseqenlem1  10058  fseqdom  10060  infpwfien  10096  fin23lem17  10370  fin23lem39  10382  isf34lem6  10412  gruurn  10830  intgru  10846  grutsk1  10853  hashfacenOLD  14465  wrdval  14518  wrdnval  14546  vdwlem4  16979  vdwlem9  16984  vdwlem10  16985  vdwlem11  16986  vdwlem13  16988  vdw  16989  vdwnnlem1  16990  rami  17010  ramcl  17024  prmgaplcm  17055  pwselbasb  17496  funcestrcsetclem7  18163  funcestrcsetclem8  18164  fullestrcsetc  18168  funcsetcestrclem8  18179  funcsetcestrclem9  18180  fullsetcestrc  18183  mndvcl  18780  gsummptnn0fz  19978  isrnghm  20417  rnghmsscmap2  20601  rnghmsscmap  20602  funcrngcsetc  20612  funcrngcsetcALT  20613  rhmsscmap2  20630  rhmsscmap  20631  funcringcsetc  20646  frlmbasf  21752  frlmsplit2  21765  uvcff  21783  psrbag  21908  evlsval2  22096  coe1fsupp  22198  gsummoncoe1  22294  evls1sca  22309  mamucl  22387  mamuvs1  22391  mamuvs2  22392  matbas2d  22411  matecl  22413  mamumat1cl  22427  mattposcl  22441  tposmap  22445  mat1dimelbas  22459  mavmulcl  22535  mdetunilem9  22608  pmatcollpw3lem  22771  pmatcollpw3fi1lem2  22775  cpmidpmatlem2  22859  cpmadumatpolylem1  22869  cayhamlem3  22875  cayhamlem4  22876  iscn  23225  iscnp  23227  cndis  23281  cnindis  23282  hausmapdom  23490  xkoptsub  23644  pt1hmeo  23796  flfval  23980  fcfval  24023  tmdgsum2  24086  symgtgp  24096  isucn  24269  ispsmet  24296  ismet  24315  isxmet  24316  imasdsf1olem  24365  elcncf  24895  metcld2  25321  elply2  26218  plyf  26220  elplyr  26223  plyeq0lem  26232  plyeq0  26233  plyaddlem  26237  plymullem  26238  dgrlem  26251  coeidlem  26259  ulmval  26404  ulmss  26421  ulmcn  26423  mtest  26428  pserulm  26446  isch2  31151  fmptco1f1o  32548  resf1o  32642  fedgmullem2  33529  smatrcl  33622  indf1ofs  33870  imambfm  34107  mbfmcnt  34113  isrrvv  34288  reprsuc  34472  reprinrn  34475  reprlt  34476  reprgt  34478  reprinfz1  34479  reprpmtf1o  34483  reprdifc  34484  circlevma  34499  deranglem  35005  indispconn  35073  prv1n  35270  knoppcnlem5  36211  knoppcnlem8  36214  curf  37310  matunitlindflem1  37328  matunitlindflem2  37329  matunitlindf  37330  fvopabf4g  37434  sdclem2  37454  sdclem1  37455  ismtyval  37512  rrncmslem  37544  aks6d1c2lem3  41836  aks6d1c5lem3  41847  aks6d1c5lem2  41848  sticksstones23  41879  evlsval3  42247  mapfzcons  42408  mzpindd  42438  mzpsubst  42440  mzprename  42441  diophrw  42451  pw2f1ocnv  42730  ofoafg  43055  snelmap  44718  fvmap  44839  difmap  44848  mapssbi  44854  fourierdlem54  45815  fourierdlem111  45872  etransclem25  45914  qndenserrnbllem  45949  elhoi  46197  hoiprodcl2  46210  hoicvrrex  46211  ovnlecvr  46213  ovn0lem  46220  hsphoif  46231  hoidmvval  46232  hsphoival  46234  hoidmvle  46255  ovnhoilem1  46256  ovnhoilem2  46257  ovnlecvr2  46265  ovncvr2  46266  hoidifhspval2  46270  hoiqssbllem3  46279  hspmbllem2  46282  opnvonmbllem1  46287  nnsum3primesgbe  47398  nnsum4primesodd  47402  nnsum4primesoddALTV  47403  nnsum4primeseven  47406  nnsum4primesevenALTV  47407  isclintop  47618  funcringcsetcALTV2lem8  47708  funcringcsetclem8ALTV  47731  ofaddmndmap  47756  mapsnop  47757  zlmodzxzel  47768  linccl  47831  lincvalsc0  47838  lcoc0  47839  linc0scn0  47840  lincdifsn  47841  linc1  47842  lincsum  47846  lincscm  47847  lincscmcl  47849  lcoss  47853  lincext1  47871  lindslinindimp2lem2  47876  lindsrng01  47885  snlindsntorlem  47887  lincresunit1  47894  lincresunit3  47898  zlmodzxzldeplem1  47917  naryfvalel  48052  1arympt1fv  48061  1arymaptfo  48065  2arymaptf  48074  prelrrx2  48135  line2x  48176  line2y  48177  map0cor  48256