Theorem elmapg 8834

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 8831	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑m 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2848	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7931	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1141	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1138	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6683	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3643	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 18	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 282	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2142  {cab 2740  Vcvv 3454  ⟶wf 6532  (class class class)co 7412   ↑_m cmap 8822

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-pow 5335  ax-pr 5403  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-sbc 3744  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7415  df-oprab 7416  df-mpo 7417  df-map 8824

This theorem is used by:  elmapd  8835  mapdm0  8837  elmapi  8844  elmap  8867  map0g  8880  fdiagfn  8886  ralxpmap  8892  ixpssmap2g  8923  snmapen  9033  pw2f1olem  9067  mapxpen  9129  fseqenlem1  10015  fseqdom  10017  infpwfien  10053  fin23lem17  10328  fin23lem39  10340  isf34lem6  10370  gruurn  10789  intgru  10805  grutsk1  10812  wrdval  14560  wrdnval  14589  vdwlem4  17050  vdwlem9  17055  vdwlem10  17056  vdwlem11  17057  vdwlem13  17059  vdw  17060  vdwnnlem1  17061  rami  17081  ramcl  17095  prmgaplcm  17126  pwselbasb  17547  funcestrcsetclem7  18208  funcestrcsetclem8  18209  fullestrcsetc  18213  funcsetcestrclem8  18224  funcsetcestrclem9  18225  fullsetcestrc  18228  mndvcl  18861  gsummptnn0fz  20062  isrnghm  20530  rnghmsscmap2  20739  rnghmsscmap  20740  funcrngcsetc  20750  funcrngcsetcALT  20751  rhmsscmap2  20768  rhmsscmap  20769  funcringcsetc  20784  frlmbasf  21921  frlmsplit2  21934  uvcff  21952  psrbag  22078  evlsval2  22249  evlsval3  22251  coe1fsupp  22385  gsummoncoe1  22479  evls1sca  22494  mamucl  22569  mamuvs1  22573  mamuvs2  22574  matbas2d  22591  matecl  22593  mamumat1cl  22607  mattposcl  22621  tposmap  22625  mat1dimelbas  22639  mavmulcl  22715  mdetunilem9  22788  pmatcollpw3lem  22951  pmatcollpw3fi1lem2  22955  cpmidpmatlem2  23039  cpmadumatpolylem1  23049  cayhamlem3  23055  cayhamlem4  23056  iscn  23403  iscnp  23405  cndis  23459  cnindis  23460  hausmapdom  23668  xkoptsub  23822  pt1hmeo  23974  flfval  24158  fcfval  24201  tmdgsum2  24264  symgtgp  24274  isucn  24445  ispsmet  24472  ismet  24491  isxmet  24492  imasdsf1olem  24541  elcncf  25059  metcld2  25477  elply2  26364  plyf  26366  elplyr  26369  plyeq0lem  26378  plyeq0  26379  plyaddlem  26383  plymullem  26384  dgrlem  26397  coeidlem  26405  ulmval  26554  ulmss  26571  ulmcn  26573  mtest  26578  pserulm  26596  isch2  31586  fmptco1f1o  32989  resf1o  33086  indf1ofs  33197  fedgmullem2  34029  smatrcl  34195  imambfm  34661  mbfmcnt  34667  isrrvv  34842  reprsuc  35011  reprinrn  35014  reprlt  35015  reprgt  35017  reprinfz1  35018  reprpmtf1o  35022  reprdifc  35023  circlevma  35038  deranglem  35666  indispconn  35734  prv1n  35931  knoppcnlem5  37114  knoppcnlem8  37117  curf  38277  matunitlindflem1  38295  matunitlindflem2  38296  matunitlindf  38297  fvopabf4g  38401  sdclem2  38421  sdclem1  38422  ismtyval  38479  rrncmslem  38511  aks6d1c2lem3  42921  aks6d1c5lem3  42932  aks6d1c5lem2  42933  sticksstones23  42964  mapfzcons  43475  mzpindd  43505  mzpsubst  43507  mzprename  43508  diophrw  43518  pw2f1ocnv  43792  ofoafg  44109  snelmap  45830  fvmap  45943  difmap  45951  mapssbi  45957  fourierdlem54  46902  fourierdlem111  46959  etransclem25  47001  qndenserrnbllem  47036  elhoi  47284  hoiprodcl2  47297  hoicvrrex  47298  ovnlecvr  47300  ovn0lem  47307  hsphoif  47318  hoidmvval  47319  hsphoival  47321  hoidmvle  47342  ovnhoilem1  47343  ovnhoilem2  47344  ovnlecvr2  47352  ovncvr2  47353  hoidifhspval2  47357  hoiqssbllem3  47366  hspmbllem2  47369  opnvonmbllem1  47374  nnsum3primesgbe  48585  nnsum4primesodd  48589  nnsum4primesoddALTV  48590  nnsum4primeseven  48593  nnsum4primesevenALTV  48594  isclintop  49000  funcringcsetcALTV2lem8  49090  funcringcsetclem8ALTV  49113  ofaddmndmap  49151  mapsnop  49152  zlmodzxzel  49163  linccl  49222  lincvalsc0  49229  lcoc0  49230  linc0scn0  49231  lincdifsn  49232  linc1  49233  lincsum  49237  lincscm  49238  lincscmcl  49240  lcoss  49244  lincext1  49262  lindslinindimp2lem2  49267  lindsrng01  49276  snlindsntorlem  49278  lincresunit1  49285  lincresunit3  49289  zlmodzxzldeplem1  49308  naryfvalel  49438  1arympt1fv  49447  1arymaptfo  49451  2arymaptf  49460  prelrrx2  49521  line2x  49562  line2y  49563  map0cor  49661