Theorem elmapg 8773

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  {cab 2707  Vcvv 3438  ⟶wf 6482  (class class class)co 7353   ↑_m cmap 8760

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494  df-ov 7356  df-oprab 7357  df-mpo 7358  df-map 8762

This theorem is referenced by:  elmapd  8774  mapdm0  8776  elmapi  8783  elmap  8805  map0g  8818  fdiagfn  8824  ralxpmap  8830  ixpssmap2g  8861  snmapen  8970  pw2f1olem  9005  mapxpen  9067  fseqenlem1  9937  fseqdom  9939  infpwfien  9975  fin23lem17  10251  fin23lem39  10263  isf34lem6  10293  gruurn  10711  intgru  10727  grutsk1  10734  wrdval  14441  wrdnval  14470  vdwlem4  16914  vdwlem9  16919  vdwlem10  16920  vdwlem11  16921  vdwlem13  16923  vdw  16924  vdwnnlem1  16925  rami  16945  ramcl  16959  prmgaplcm  16990  pwselbasb  17410  funcestrcsetclem7  18070  funcestrcsetclem8  18071  fullestrcsetc  18075  funcsetcestrclem8  18086  funcsetcestrclem9  18087  fullsetcestrc  18090  mndvcl  18689  gsummptnn0fz  19883  isrnghm  20344  rnghmsscmap2  20532  rnghmsscmap  20533  funcrngcsetc  20543  funcrngcsetcALT  20544  rhmsscmap2  20561  rhmsscmap  20562  funcringcsetc  20577  frlmbasf  21685  frlmsplit2  21698  uvcff  21716  psrbag  21842  evlsval2  22010  coe1fsupp  22115  gsummoncoe1  22211  evls1sca  22226  mamucl  22304  mamuvs1  22308  mamuvs2  22309  matbas2d  22326  matecl  22328  mamumat1cl  22342  mattposcl  22356  tposmap  22360  mat1dimelbas  22374  mavmulcl  22450  mdetunilem9  22523  pmatcollpw3lem  22686  pmatcollpw3fi1lem2  22690  cpmidpmatlem2  22774  cpmadumatpolylem1  22784  cayhamlem3  22790  cayhamlem4  22791  iscn  23138  iscnp  23140  cndis  23194  cnindis  23195  hausmapdom  23403  xkoptsub  23557  pt1hmeo  23709  flfval  23893  fcfval  23936  tmdgsum2  23999  symgtgp  24009  isucn  24181  ispsmet  24208  ismet  24227  isxmet  24228  imasdsf1olem  24277  elcncf  24798  metcld2  25223  elply2  26117  plyf  26119  elplyr  26122  plyeq0lem  26131  plyeq0  26132  plyaddlem  26136  plymullem  26137  dgrlem  26150  coeidlem  26158  ulmval  26305  ulmss  26322  ulmcn  26324  mtest  26329  pserulm  26347  isch2  31185  fmptco1f1o  32590  resf1o  32686  indf1ofs  32822  fedgmullem2  33602  smatrcl  33762  imambfm  34229  mbfmcnt  34235  isrrvv  34410  reprsuc  34582  reprinrn  34585  reprlt  34586  reprgt  34588  reprinfz1  34589  reprpmtf1o  34593  reprdifc  34594  circlevma  34609  deranglem  35138  indispconn  35206  prv1n  35403  knoppcnlem5  36470  knoppcnlem8  36473  curf  37577  matunitlindflem1  37595  matunitlindflem2  37596  matunitlindf  37597  fvopabf4g  37701  sdclem2  37721  sdclem1  37722  ismtyval  37779  rrncmslem  37811  aks6d1c2lem3  42099  aks6d1c5lem3  42110  aks6d1c5lem2  42111  sticksstones23  42142  evlsval3  42532  mapfzcons  42689  mzpindd  42719  mzpsubst  42721  mzprename  42722  diophrw  42732  pw2f1ocnv  43010  ofoafg  43327  snelmap  45060  fvmap  45176  difmap  45185  mapssbi  45191  fourierdlem54  46142  fourierdlem111  46199  etransclem25  46241  qndenserrnbllem  46276  elhoi  46524  hoiprodcl2  46537  hoicvrrex  46538  ovnlecvr  46540  ovn0lem  46547  hsphoif  46558  hoidmvval  46559  hsphoival  46561  hoidmvle  46582  ovnhoilem1  46583  ovnhoilem2  46584  ovnlecvr2  46592  ovncvr2  46593  hoidifhspval2  46597  hoiqssbllem3  46606  hspmbllem2  46609  opnvonmbllem1  46614  nnsum3primesgbe  47777  nnsum4primesodd  47781  nnsum4primesoddALTV  47782  nnsum4primeseven  47785  nnsum4primesevenALTV  47786  isclintop  48192  funcringcsetcALTV2lem8  48282  funcringcsetclem8ALTV  48305  ofaddmndmap  48328  mapsnop  48329  zlmodzxzel  48340  linccl  48400  lincvalsc0  48407  lcoc0  48408  linc0scn0  48409  lincdifsn  48410  linc1  48411  lincsum  48415  lincscm  48416  lincscmcl  48418  lcoss  48422  lincext1  48440  lindslinindimp2lem2  48445  lindsrng01  48454  snlindsntorlem  48456  lincresunit1  48463  lincresunit3  48467  zlmodzxzldeplem1  48486  naryfvalel  48616  1arympt1fv  48625  1arymaptfo  48629  2arymaptf  48638  prelrrx2  48699  line2x  48740  line2y  48741  map0cor  48840