Theorem elmapg 8897

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  {cab 2717  Vcvv 3488  ⟶wf 6569  (class class class)co 7448   ↑_m cmap 8884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-map 8886

This theorem is referenced by:  elmapd  8898  mapdm0  8900  elmapi  8907  elmap  8929  map0g  8942  fdiagfn  8948  ralxpmap  8954  ixpssmap2g  8985  snmapen  9103  pw2f1olem  9142  mapxpen  9209  fseqenlem1  10093  fseqdom  10095  infpwfien  10131  fin23lem17  10407  fin23lem39  10419  isf34lem6  10449  gruurn  10867  intgru  10883  grutsk1  10890  wrdval  14565  wrdnval  14593  vdwlem4  17031  vdwlem9  17036  vdwlem10  17037  vdwlem11  17038  vdwlem13  17040  vdw  17041  vdwnnlem1  17042  rami  17062  ramcl  17076  prmgaplcm  17107  pwselbasb  17548  funcestrcsetclem7  18215  funcestrcsetclem8  18216  fullestrcsetc  18220  funcsetcestrclem8  18231  funcsetcestrclem9  18232  fullsetcestrc  18235  mndvcl  18832  gsummptnn0fz  20028  isrnghm  20467  rnghmsscmap2  20651  rnghmsscmap  20652  funcrngcsetc  20662  funcrngcsetcALT  20663  rhmsscmap2  20680  rhmsscmap  20681  funcringcsetc  20696  frlmbasf  21803  frlmsplit2  21816  uvcff  21834  psrbag  21960  evlsval2  22134  coe1fsupp  22237  gsummoncoe1  22333  evls1sca  22348  mamucl  22426  mamuvs1  22430  mamuvs2  22431  matbas2d  22450  matecl  22452  mamumat1cl  22466  mattposcl  22480  tposmap  22484  mat1dimelbas  22498  mavmulcl  22574  mdetunilem9  22647  pmatcollpw3lem  22810  pmatcollpw3fi1lem2  22814  cpmidpmatlem2  22898  cpmadumatpolylem1  22908  cayhamlem3  22914  cayhamlem4  22915  iscn  23264  iscnp  23266  cndis  23320  cnindis  23321  hausmapdom  23529  xkoptsub  23683  pt1hmeo  23835  flfval  24019  fcfval  24062  tmdgsum2  24125  symgtgp  24135  isucn  24308  ispsmet  24335  ismet  24354  isxmet  24355  imasdsf1olem  24404  elcncf  24934  metcld2  25360  elply2  26255  plyf  26257  elplyr  26260  plyeq0lem  26269  plyeq0  26270  plyaddlem  26274  plymullem  26275  dgrlem  26288  coeidlem  26296  ulmval  26441  ulmss  26458  ulmcn  26460  mtest  26465  pserulm  26483  isch2  31255  fmptco1f1o  32652  resf1o  32744  fedgmullem2  33643  smatrcl  33742  indf1ofs  33990  imambfm  34227  mbfmcnt  34233  isrrvv  34408  reprsuc  34592  reprinrn  34595  reprlt  34596  reprgt  34598  reprinfz1  34599  reprpmtf1o  34603  reprdifc  34604  circlevma  34619  deranglem  35134  indispconn  35202  prv1n  35399  knoppcnlem5  36463  knoppcnlem8  36466  curf  37558  matunitlindflem1  37576  matunitlindflem2  37577  matunitlindf  37578  fvopabf4g  37682  sdclem2  37702  sdclem1  37703  ismtyval  37760  rrncmslem  37792  aks6d1c2lem3  42083  aks6d1c5lem3  42094  aks6d1c5lem2  42095  sticksstones23  42126  evlsval3  42514  mapfzcons  42672  mzpindd  42702  mzpsubst  42704  mzprename  42705  diophrw  42715  pw2f1ocnv  42994  ofoafg  43316  snelmap  44984  fvmap  45105  difmap  45114  mapssbi  45120  fourierdlem54  46081  fourierdlem111  46138  etransclem25  46180  qndenserrnbllem  46215  elhoi  46463  hoiprodcl2  46476  hoicvrrex  46477  ovnlecvr  46479  ovn0lem  46486  hsphoif  46497  hoidmvval  46498  hsphoival  46500  hoidmvle  46521  ovnhoilem1  46522  ovnhoilem2  46523  ovnlecvr2  46531  ovncvr2  46532  hoidifhspval2  46536  hoiqssbllem3  46545  hspmbllem2  46548  opnvonmbllem1  46553  nnsum3primesgbe  47666  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  isclintop  47930  funcringcsetcALTV2lem8  48020  funcringcsetclem8ALTV  48043  ofaddmndmap  48068  mapsnop  48069  zlmodzxzel  48080  linccl  48143  lincvalsc0  48150  lcoc0  48151  linc0scn0  48152  lincdifsn  48153  linc1  48154  lincsum  48158  lincscm  48159  lincscmcl  48161  lcoss  48165  lincext1  48183  lindslinindimp2lem2  48188  lindsrng01  48197  snlindsntorlem  48199  lincresunit1  48206  lincresunit3  48210  zlmodzxzldeplem1  48229  naryfvalel  48364  1arympt1fv  48373  1arymaptfo  48377  2arymaptf  48386  prelrrx2  48447  line2x  48488  line2y  48489  map0cor  48568