Theorem elmapg 8862

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 8859	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑m 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2846	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7948	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1142	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1139	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6687	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3638	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 18	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 282	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2144  {cab 2738  Vcvv 3450  ⟶wf 6534  (class class class)co 7420   ↑_m cmap 8850

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-map 8852

This theorem is used by:  elmapd  8863  mapdm0  8865  elmapi  8872  curf  8893  elmap  8902  map0g  8915  fdiagfn  8921  ralxpmap  8927  ixpssmap2g  8958  snmapen  9069  pw2f1olem  9103  mapxpen  9165  fseqenlem1  10106  fseqdom  10108  infpwfien  10144  fin23lem17  10419  fin23lem39  10431  isf34lem6  10461  gruurn  10886  intgru  10902  grutsk1  10909  wrdval  14664  wrdnval  14693  vdwlem4  17167  vdwlem9  17172  vdwlem10  17173  vdwlem11  17174  vdwlem13  17176  vdw  17177  vdwnnlem1  17178  rami  17198  ramcl  17212  prmgaplcm  17243  pwselbasb  17664  funcestrcsetclem7  18325  funcestrcsetclem8  18326  fullestrcsetc  18330  funcsetcestrclem8  18341  funcsetcestrclem9  18342  fullsetcestrc  18345  mndvcl  18997  gsummptnn0fz  20205  isrnghm  20676  rnghmsscmap2  20886  rnghmsscmap  20887  funcrngcsetc  20897  funcrngcsetcALT  20898  rhmsscmap2  20915  rhmsscmap  20916  funcringcsetc  20931  frlmbasf  22071  frlmsplit2  22084  uvcff  22102  psrbag  22230  evlsval2  22401  evlsval3  22403  coe1fsupp  22537  gsummoncoe1  22631  evls1sca  22646  mamucl  22721  mamuvs1  22725  mamuvs2  22726  matbas2d  22743  matecl  22745  mamumat1cl  22759  mattposcl  22773  tposmap  22777  mat1dimelbas  22791  mavmulcl  22867  mdetunilem9  22940  matunitlindflem1  22999  matunitlindflem2  23000  matunitlindf  23001  pmatcollpw3lem  23106  pmatcollpw3fi1lem2  23110  cpmidpmatlem2  23194  cpmadumatpolylem1  23204  cayhamlem3  23210  cayhamlem4  23211  iscn  23558  iscnp  23560  cndis  23614  cnindis  23615  hausmapdom  23824  xkoptsub  23978  pt1hmeo  24130  flfval  24314  fcfval  24357  tmdgsum2  24420  symgtgp  24430  isucn  24601  ispsmet  24628  ismet  24647  isxmet  24648  imasdsf1olem  24697  elcncf  25215  metcld2  25633  elply2  26519  plyf  26521  elplyr  26524  plyeq0lem  26534  plyeq0  26535  plyaddlem  26539  plymullem  26540  dgrlem  26553  coeidlem  26561  ulmval  26712  ulmss  26729  ulmcn  26731  mtest  26736  pserulm  26754  isch2  31830  fmptco1f1o  33274  resf1o  33368  indf1ofs  33479  fedgmullem2  34308  smatrcl  34474  imambfm  34940  mbfmcnt  34946  isrrvv  35121  reprsuc  35290  reprinrn  35293  reprlt  35294  reprgt  35296  reprinfz1  35297  reprpmtf1o  35301  reprdifc  35302  circlevma  35317  deranglem  36017  indispconn  36085  prv1n  36282  knoppcnlem5  37455  knoppcnlem8  37458  fvopabf4g  38749  sdclem2  38769  sdclem1  38770  ismtyval  38827  rrncmslem  38859  aks6d1c2lem3  43269  aks6d1c5lem3  43280  aks6d1c5lem2  43281  sticksstones23  43312  mapfzcons  43820  mzpindd  43850  mzpsubst  43852  mzprename  43853  diophrw  43863  pw2f1ocnv  44137  ofoafg  44449  snelmap  46192  fvmap  46305  difmap  46313  mapssbi  46319  fourierdlem54  47263  fourierdlem111  47320  etransclem25  47362  qndenserrnbllem  47397  elhoi  47645  hoiprodcl2  47658  hoicvrrex  47659  ovnlecvr  47661  ovn0lem  47668  hsphoif  47679  hoidmvval  47680  hsphoival  47682  hoidmvle  47703  ovnhoilem1  47704  ovnhoilem2  47705  ovnlecvr2  47713  ovncvr2  47714  hoidifhspval2  47718  hoiqssbllem3  47727  hspmbllem2  47730  opnvonmbllem1  47735  nnsum3primesgbe  48983  nnsum4primesodd  48987  nnsum4primesoddALTV  48988  nnsum4primeseven  48991  nnsum4primesevenALTV  48992  isclintop  49397  funcringcsetcALTV2lem8  49487  funcringcsetclem8ALTV  49510  ofaddmndmap  49548  mapsnop  49549  zlmodzxzel  49560  linccl  49619  lincvalsc0  49626  lcoc0  49627  linc0scn0  49628  lincdifsn  49629  linc1  49630  lincsum  49634  lincscm  49635  lincscmcl  49637  lcoss  49641  lincext1  49659  lindslinindimp2lem2  49664  lindsrng01  49673  snlindsntorlem  49675  lincresunit1  49682  lincresunit3  49686  zlmodzxzldeplem1  49705  naryfvalel  49835  1arympt1fv  49844  1arymaptfo  49848  2arymaptf  49857  line2x  49959  line2y  49960  map0cor  50059