Theorem elmapg 8786

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 8783	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑m 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2822	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7887	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1125	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1122	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6646	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3628	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 279	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  {cab 2714  Vcvv 3429  ⟶wf 6494  (class class class)co 7367   ↑_m cmap 8773

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-map 8775

This theorem is referenced by:  elmapd  8787  mapdm0  8789  elmapi  8796  elmap  8819  map0g  8832  fdiagfn  8838  ralxpmap  8844  ixpssmap2g  8875  snmapen  8985  pw2f1olem  9019  mapxpen  9081  fseqenlem1  9946  fseqdom  9948  infpwfien  9984  fin23lem17  10260  fin23lem39  10272  isf34lem6  10302  gruurn  10721  intgru  10737  grutsk1  10744  wrdval  14478  wrdnval  14507  vdwlem4  16955  vdwlem9  16960  vdwlem10  16961  vdwlem11  16962  vdwlem13  16964  vdw  16965  vdwnnlem1  16966  rami  16986  ramcl  17000  prmgaplcm  17031  pwselbasb  17451  funcestrcsetclem7  18112  funcestrcsetclem8  18113  fullestrcsetc  18117  funcsetcestrclem8  18128  funcsetcestrclem9  18129  fullsetcestrc  18132  mndvcl  18765  gsummptnn0fz  19961  isrnghm  20421  rnghmsscmap2  20606  rnghmsscmap  20607  funcrngcsetc  20617  funcrngcsetcALT  20618  rhmsscmap2  20635  rhmsscmap  20636  funcringcsetc  20651  frlmbasf  21740  frlmsplit2  21753  uvcff  21771  psrbag  21897  evlsval2  22065  evlsval3  22067  coe1fsupp  22178  gsummoncoe1  22273  evls1sca  22288  mamucl  22366  mamuvs1  22370  mamuvs2  22371  matbas2d  22388  matecl  22390  mamumat1cl  22404  mattposcl  22418  tposmap  22422  mat1dimelbas  22436  mavmulcl  22512  mdetunilem9  22585  pmatcollpw3lem  22748  pmatcollpw3fi1lem2  22752  cpmidpmatlem2  22836  cpmadumatpolylem1  22846  cayhamlem3  22852  cayhamlem4  22853  iscn  23200  iscnp  23202  cndis  23256  cnindis  23257  hausmapdom  23465  xkoptsub  23619  pt1hmeo  23771  flfval  23955  fcfval  23998  tmdgsum2  24061  symgtgp  24071  isucn  24242  ispsmet  24269  ismet  24288  isxmet  24289  imasdsf1olem  24338  elcncf  24856  metcld2  25274  elply2  26161  plyf  26163  elplyr  26166  plyeq0lem  26175  plyeq0  26176  plyaddlem  26180  plymullem  26181  dgrlem  26194  coeidlem  26202  ulmval  26345  ulmss  26362  ulmcn  26364  mtest  26369  pserulm  26387  isch2  31294  fmptco1f1o  32706  resf1o  32803  indf1ofs  32926  fedgmullem2  33774  smatrcl  33940  imambfm  34406  mbfmcnt  34412  isrrvv  34587  reprsuc  34759  reprinrn  34762  reprlt  34763  reprgt  34765  reprinfz1  34766  reprpmtf1o  34770  reprdifc  34771  circlevma  34786  deranglem  35348  indispconn  35416  prv1n  35613  knoppcnlem5  36757  knoppcnlem8  36760  curf  37919  matunitlindflem1  37937  matunitlindflem2  37938  matunitlindf  37939  fvopabf4g  38043  sdclem2  38063  sdclem1  38064  ismtyval  38121  rrncmslem  38153  aks6d1c2lem3  42565  aks6d1c5lem3  42576  aks6d1c5lem2  42577  sticksstones23  42608  mapfzcons  43148  mzpindd  43178  mzpsubst  43180  mzprename  43181  diophrw  43191  pw2f1ocnv  43465  ofoafg  43782  snelmap  45513  fvmap  45627  difmap  45636  mapssbi  45642  fourierdlem54  46588  fourierdlem111  46645  etransclem25  46687  qndenserrnbllem  46722  elhoi  46970  hoiprodcl2  46983  hoicvrrex  46984  ovnlecvr  46986  ovn0lem  46993  hsphoif  47004  hoidmvval  47005  hsphoival  47007  hoidmvle  47028  ovnhoilem1  47029  ovnhoilem2  47030  ovnlecvr2  47038  ovncvr2  47039  hoidifhspval2  47043  hoiqssbllem3  47052  hspmbllem2  47055  opnvonmbllem1  47060  nnsum3primesgbe  48268  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  isclintop  48683  funcringcsetcALTV2lem8  48773  funcringcsetclem8ALTV  48796  ofaddmndmap  48819  mapsnop  48820  zlmodzxzel  48831  linccl  48890  lincvalsc0  48897  lcoc0  48898  linc0scn0  48899  lincdifsn  48900  linc1  48901  lincsum  48905  lincscm  48906  lincscmcl  48908  lcoss  48912  lincext1  48930  lindslinindimp2lem2  48935  lindsrng01  48944  snlindsntorlem  48946  lincresunit1  48953  lincresunit3  48957  zlmodzxzldeplem1  48976  naryfvalel  49106  1arympt1fv  49115  1arymaptfo  49119  2arymaptf  49128  prelrrx2  49189  line2x  49230  line2y  49231  map0cor  49330