Theorem elmapg 8637

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 8634	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑m 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2825	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7789	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1123	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1120	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6590	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3617	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 278	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∈ wcel 2107  {cab 2716  Vcvv 3433  ⟶wf 6433  (class class class)co 7284   ↑_m cmap 8624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289  df-map 8626

This theorem is referenced by:  elmapd  8638  mapdm0  8639  elmapi  8646  elmap  8668  map0g  8681  fdiagfn  8687  ralxpmap  8693  ixpssmap2g  8724  snmapen  8837  pw2f1olem  8872  mapxpen  8939  fseqenlem1  9789  fseqdom  9791  infpwfien  9827  fin23lem17  10103  fin23lem39  10115  isf34lem6  10145  gruurn  10563  intgru  10579  grutsk1  10586  hashfacenOLD  14176  wrdval  14229  wrdnval  14257  vdwlem4  16694  vdwlem9  16699  vdwlem10  16700  vdwlem11  16701  vdwlem13  16703  vdw  16704  vdwnnlem1  16705  rami  16725  ramcl  16739  prmgaplcm  16770  pwselbasb  17208  funcestrcsetclem7  17872  funcestrcsetclem8  17873  fullestrcsetc  17877  funcsetcestrclem8  17888  funcsetcestrclem9  17889  fullsetcestrc  17892  gsummptnn0fz  19596  frlmbasf  20976  frlmsplit2  20989  uvcff  21007  psrbag  21129  evlsval2  21306  coe1fsupp  21394  gsummoncoe1  21484  evls1sca  21498  mndvcl  21549  mamucl  21557  mamuvs1  21561  mamuvs2  21562  matbas2d  21581  matecl  21583  mamumat1cl  21597  mattposcl  21611  tposmap  21615  mat1dimelbas  21629  mavmulcl  21705  mdetunilem9  21778  pmatcollpw3lem  21941  pmatcollpw3fi1lem2  21945  cpmidpmatlem2  22029  cpmadumatpolylem1  22039  cayhamlem3  22045  cayhamlem4  22046  iscn  22395  iscnp  22397  cndis  22451  cnindis  22452  hausmapdom  22660  xkoptsub  22814  pt1hmeo  22966  flfval  23150  fcfval  23193  tmdgsum2  23256  symgtgp  23266  isucn  23439  ispsmet  23466  ismet  23485  isxmet  23486  imasdsf1olem  23535  elcncf  24061  metcld2  24480  elply2  25366  plyf  25368  elplyr  25371  plyeq0lem  25380  plyeq0  25381  plyaddlem  25385  plymullem  25386  dgrlem  25399  coeidlem  25407  ulmval  25548  ulmss  25565  ulmcn  25567  mtest  25572  pserulm  25590  isch2  29594  fmptco1f1o  30977  resf1o  31074  fedgmullem2  31720  smatrcl  31755  indf1ofs  32003  imambfm  32238  mbfmcnt  32244  isrrvv  32419  reprsuc  32604  reprinrn  32607  reprlt  32608  reprgt  32610  reprinfz1  32611  reprpmtf1o  32615  reprdifc  32616  circlevma  32631  deranglem  33137  indispconn  33205  prv1n  33402  knoppcnlem5  34686  knoppcnlem8  34689  curf  35764  matunitlindflem1  35782  matunitlindflem2  35783  matunitlindf  35784  fvopabf4g  35888  sdclem2  35909  sdclem1  35910  ismtyval  35967  rrncmslem  35999  evlsval3  40279  mapfzcons  40545  mzpindd  40575  mzpsubst  40577  mzprename  40578  diophrw  40588  pw2f1ocnv  40866  snelmap  42639  fvmap  42744  difmap  42754  mapssbi  42760  fourierdlem54  43708  fourierdlem111  43765  etransclem25  43807  qndenserrnbllem  43842  elhoi  44087  hoiprodcl2  44100  hoicvrrex  44101  ovnlecvr  44103  ovn0lem  44110  hsphoif  44121  hoidmvval  44122  hsphoival  44124  hoidmvle  44145  ovnhoilem1  44146  ovnhoilem2  44147  ovnlecvr2  44155  ovncvr2  44156  hoidifhspval2  44160  hoiqssbllem3  44169  hspmbllem2  44172  opnvonmbllem1  44177  nnsum3primesgbe  45255  nnsum4primesodd  45259  nnsum4primesoddALTV  45260  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  isclintop  45412  isrnghm  45461  rnghmsscmap2  45542  rnghmsscmap  45543  funcrngcsetc  45567  funcrngcsetcALT  45568  rhmsscmap2  45588  rhmsscmap  45589  funcringcsetc  45604  funcringcsetcALTV2lem8  45612  funcringcsetclem8ALTV  45635  ofaddmndmap  45690  mapsnop  45691  zlmodzxzel  45702  linccl  45766  lincvalsc0  45773  lcoc0  45774  linc0scn0  45775  lincdifsn  45776  linc1  45777  lincsum  45781  lincscm  45782  lincscmcl  45784  lcoss  45788  lincext1  45806  lindslinindimp2lem2  45811  lindsrng01  45820  snlindsntorlem  45822  lincresunit1  45829  lincresunit3  45833  zlmodzxzldeplem1  45852  naryfvalel  45987  1arympt1fv  45996  1arymaptfo  46000  2arymaptf  46009  prelrrx2  46070  line2x  46111  line2y  46112  map0cor  46193