Theorem elmapg 8832

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 8829	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑m 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2819	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7923	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1124	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1121	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6698	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3675	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 278	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  {cab 2709  Vcvv 3474  ⟶wf 6539  (class class class)co 7408   ↑_m cmap 8819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-map 8821

This theorem is referenced by:  elmapd  8833  mapdm0  8835  elmapi  8842  elmap  8864  map0g  8877  fdiagfn  8883  ralxpmap  8889  ixpssmap2g  8920  snmapen  9037  pw2f1olem  9075  mapxpen  9142  fseqenlem1  10018  fseqdom  10020  infpwfien  10056  fin23lem17  10332  fin23lem39  10344  isf34lem6  10374  gruurn  10792  intgru  10808  grutsk1  10815  hashfacenOLD  14413  wrdval  14466  wrdnval  14494  vdwlem4  16916  vdwlem9  16921  vdwlem10  16922  vdwlem11  16923  vdwlem13  16925  vdw  16926  vdwnnlem1  16927  rami  16947  ramcl  16961  prmgaplcm  16992  pwselbasb  17433  funcestrcsetclem7  18097  funcestrcsetclem8  18098  fullestrcsetc  18102  funcsetcestrclem8  18113  funcsetcestrclem9  18114  fullsetcestrc  18117  gsummptnn0fz  19853  frlmbasf  21314  frlmsplit2  21327  uvcff  21345  psrbag  21469  evlsval2  21649  coe1fsupp  21737  gsummoncoe1  21827  evls1sca  21841  mndvcl  21892  mamucl  21900  mamuvs1  21904  mamuvs2  21905  matbas2d  21924  matecl  21926  mamumat1cl  21940  mattposcl  21954  tposmap  21958  mat1dimelbas  21972  mavmulcl  22048  mdetunilem9  22121  pmatcollpw3lem  22284  pmatcollpw3fi1lem2  22288  cpmidpmatlem2  22372  cpmadumatpolylem1  22382  cayhamlem3  22388  cayhamlem4  22389  iscn  22738  iscnp  22740  cndis  22794  cnindis  22795  hausmapdom  23003  xkoptsub  23157  pt1hmeo  23309  flfval  23493  fcfval  23536  tmdgsum2  23599  symgtgp  23609  isucn  23782  ispsmet  23809  ismet  23828  isxmet  23829  imasdsf1olem  23878  elcncf  24404  metcld2  24823  elply2  25709  plyf  25711  elplyr  25714  plyeq0lem  25723  plyeq0  25724  plyaddlem  25728  plymullem  25729  dgrlem  25742  coeidlem  25750  ulmval  25891  ulmss  25908  ulmcn  25910  mtest  25915  pserulm  25933  isch2  30471  fmptco1f1o  31852  resf1o  31950  ply1degltdimlem  32702  fedgmullem2  32710  smatrcl  32771  indf1ofs  33019  imambfm  33256  mbfmcnt  33262  isrrvv  33437  reprsuc  33622  reprinrn  33625  reprlt  33626  reprgt  33628  reprinfz1  33629  reprpmtf1o  33633  reprdifc  33634  circlevma  33649  deranglem  34152  indispconn  34220  prv1n  34417  knoppcnlem5  35368  knoppcnlem8  35371  curf  36461  matunitlindflem1  36479  matunitlindflem2  36480  matunitlindf  36481  fvopabf4g  36585  sdclem2  36605  sdclem1  36606  ismtyval  36663  rrncmslem  36695  evlsval3  41133  mapfzcons  41444  mzpindd  41474  mzpsubst  41476  mzprename  41477  diophrw  41487  pw2f1ocnv  41766  ofoafg  42094  snelmap  43761  fvmap  43887  difmap  43896  mapssbi  43902  fourierdlem54  44866  fourierdlem111  44923  etransclem25  44965  qndenserrnbllem  45000  elhoi  45248  hoiprodcl2  45261  hoicvrrex  45262  ovnlecvr  45264  ovn0lem  45271  hsphoif  45282  hoidmvval  45283  hsphoival  45285  hoidmvle  45306  ovnhoilem1  45307  ovnhoilem2  45308  ovnlecvr2  45316  ovncvr2  45317  hoidifhspval2  45321  hoiqssbllem3  45330  hspmbllem2  45333  opnvonmbllem1  45338  nnsum3primesgbe  46450  nnsum4primesodd  46454  nnsum4primesoddALTV  46455  nnsum4primeseven  46458  nnsum4primesevenALTV  46459  isclintop  46607  isrnghm  46680  rnghmsscmap2  46861  rnghmsscmap  46862  funcrngcsetc  46886  funcrngcsetcALT  46887  rhmsscmap2  46907  rhmsscmap  46908  funcringcsetc  46923  funcringcsetcALTV2lem8  46931  funcringcsetclem8ALTV  46954  ofaddmndmap  47009  mapsnop  47010  zlmodzxzel  47021  linccl  47085  lincvalsc0  47092  lcoc0  47093  linc0scn0  47094  lincdifsn  47095  linc1  47096  lincsum  47100  lincscm  47101  lincscmcl  47103  lcoss  47107  lincext1  47125  lindslinindimp2lem2  47130  lindsrng01  47139  snlindsntorlem  47141  lincresunit1  47148  lincresunit3  47152  zlmodzxzldeplem1  47171  naryfvalel  47306  1arympt1fv  47315  1arymaptfo  47319  2arymaptf  47328  prelrrx2  47389  line2x  47430  line2y  47431  map0cor  47511