Theorem elmapg 8073

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

Assertion

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

Proof of Theorem elmapg

Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mapvalg 8070	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑𝑚 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2830	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7319	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1154	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1150	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6204	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3512	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 270	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   ∈ wcel 2155  {cab 2751  Vcvv 3350  ⟶wf 6064  (class class class)co 6842   ↑_𝑚 cmap 8060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-opab 4872  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-fv 6076  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-map 8062

This theorem is referenced by:  elmapd  8074  mapdm0  8075  elmapi  8082  elmap  8089  map0eOLD  8099  map0g  8101  mapsnd  8102  fdiagfn  8106  ralxpmap  8112  ixpssmap2g  8142  snmapen  8241  pw2f1olem  8271  mapxpen  8333  fseqenlem1  9098  fseqdom  9100  infpwfien  9136  fin23lem17  9413  fin23lem39  9425  isf34lem6  9455  gruurn  9873  intgru  9889  grutsk1  9896  hashfacen  13439  wrdval  13489  wrdnval  13516  vdwlem4  15967  vdwlem9  15972  vdwlem10  15973  vdwlem11  15974  vdwlem13  15976  vdw  15977  vdwnnlem1  15978  rami  15998  ramcl  16012  prmgaplcm  16043  pwselbasb  16414  elestrchom  17033  estrcco  17035  funcestrcsetclem7  17052  funcestrcsetclem8  17053  fullestrcsetc  17057  funcsetcestrclem7  17067  funcsetcestrclem8  17068  funcsetcestrclem9  17069  fullsetcestrc  17072  symgbas  18063  gsummptnn0fz  18648  gsummptnn0fzOLD  18649  psrbag  19638  evlsval2  19793  coe1fsupp  19857  gsummoncoe1  19947  evls1sca  19961  frlmbasf  20380  frlmsplit2  20388  uvcff  20406  mndvcl  20473  mamucl  20483  mamuvs1  20487  mamuvs2  20488  matbas2d  20505  matecl  20507  mamumat1cl  20521  mattposcl  20536  tposmap  20540  mat1dimelbas  20554  mavmulcl  20630  mdetunilem9  20703  pmatcollpw3lem  20867  pmatcollpw3fi1lem2  20871  cpmidpmatlem2  20955  cpmadumatpolylem1  20965  cayhamlem3  20971  cayhamlem4  20972  iscn  21319  iscnp  21321  cndis  21375  cnindis  21376  hausmapdom  21583  xkoptsub  21737  pt1hmeo  21889  flfval  22073  fcfval  22116  tmdgsum2  22179  symgtgp  22184  isucn  22361  ispsmet  22388  ismet  22407  isxmet  22408  imasdsf1olem  22457  elcncf  22971  metcld2  23384  elply2  24243  plyf  24245  elplyr  24248  plyeq0lem  24257  plyeq0  24258  plyaddlem  24262  plymullem  24263  dgrlem  24276  coeidlem  24284  ulmval  24425  ulmss  24442  ulmcn  24444  mtest  24449  pserulm  24467  isch2  28536  fmptco1f1o  29884  resf1o  29954  smatrcl  30309  indf1ofs  30535  imambfm  30771  mbfmcnt  30777  isrrvv  30953  reprsuc  31144  reprinrn  31147  reprlt  31148  reprgt  31150  reprinfz1  31151  reprpmtf1o  31155  reprdifc  31156  circlevma  31171  deranglem  31596  indispconn  31664  knoppcnlem5  32926  knoppcnlem8  32929  curf  33811  matunitlindflem1  33829  matunitlindflem2  33830  matunitlindf  33831  fvopabf4g  33938  sdclem2  33960  sdclem1  33961  ismtyval  34021  rrncmslem  34053  mapfzcons  37957  mzpindd  37987  mzpsubst  37989  mzprename  37990  diophrw  38000  pw2f1ocnv  38281  snelmap  39905  mapdm0OLD  40030  fvmap  40034  difmap  40044  mapssbi  40050  fourierdlem54  41014  fourierdlem111  41071  etransclem25  41113  qndenserrnbllem  41151  elhoi  41396  hoiprodcl2  41409  hoicvrrex  41410  ovnlecvr  41412  ovn0lem  41419  hsphoif  41430  hoidmvval  41431  hsphoival  41433  hoidmvle  41454  ovnhoilem1  41455  ovnhoilem2  41456  ovnlecvr2  41464  ovncvr2  41465  hoidifhspval2  41469  hoiqssbllem3  41478  hspmbllem2  41481  opnvonmbllem1  41486  nnsum3primesgbe  42356  nnsum4primesodd  42360  nnsum4primesoddALTV  42361  nnsum4primeseven  42364  nnsum4primesevenALTV  42365  isclintop  42512  isrnghm  42561  rnghmsscmap2  42642  rnghmsscmap  42643  funcrngcsetc  42667  funcrngcsetcALT  42668  rhmsscmap2  42688  rhmsscmap  42689  funcringcsetc  42704  funcringcsetcALTV2lem8  42712  funcringcsetclem8ALTV  42735  ofaddmndmap  42791  mapsnop  42792  mapprop  42793  zlmodzxzel  42802  linccl  42872  lincvalsc0  42879  lcoc0  42880  linc0scn0  42881  lincdifsn  42882  linc1  42883  lincsum  42887  lincscm  42888  lincscmcl  42890  lcoss  42894  lincext1  42912  lindslinindimp2lem2  42917  lindsrng01  42926  snlindsntorlem  42928  lincresunit1  42935  lincresunit3  42939  zlmodzxzldeplem1  42958