Theorem elmapg 8842

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 8839	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑m 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2848	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7937	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1142	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1139	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6684	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3642	. . 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 2145  {cab 2740  Vcvv 3453  ⟶wf 6533  (class class class)co 7417   ↑_m cmap 8830

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pow 5334  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-map 8832

This theorem is used by:  elmapd  8843  mapdm0  8845  elmapi  8852  curf  8873  elmap  8882  map0g  8895  fdiagfn  8901  ralxpmap  8907  ixpssmap2g  8938  snmapen  9049  pw2f1olem  9083  mapxpen  9145  fseqenlem1  10031  fseqdom  10033  infpwfien  10069  fin23lem17  10344  fin23lem39  10356  isf34lem6  10386  gruurn  10811  intgru  10827  grutsk1  10834  wrdval  14585  wrdnval  14614  vdwlem4  17082  vdwlem9  17087  vdwlem10  17088  vdwlem11  17089  vdwlem13  17091  vdw  17092  vdwnnlem1  17093  rami  17113  ramcl  17127  prmgaplcm  17158  pwselbasb  17579  funcestrcsetclem7  18240  funcestrcsetclem8  18241  fullestrcsetc  18245  funcsetcestrclem8  18256  funcsetcestrclem9  18257  fullsetcestrc  18260  mndvcl  18911  gsummptnn0fz  20119  isrnghm  20588  rnghmsscmap2  20797  rnghmsscmap  20798  funcrngcsetc  20808  funcrngcsetcALT  20809  rhmsscmap2  20826  rhmsscmap  20827  funcringcsetc  20842  frlmbasf  21979  frlmsplit2  21992  uvcff  22010  psrbag  22138  evlsval2  22309  evlsval3  22311  coe1fsupp  22445  gsummoncoe1  22539  evls1sca  22554  mamucl  22629  mamuvs1  22633  mamuvs2  22634  matbas2d  22651  matecl  22653  mamumat1cl  22667  mattposcl  22681  tposmap  22685  mat1dimelbas  22699  mavmulcl  22775  mdetunilem9  22848  matunitlindflem1  22907  matunitlindflem2  22908  matunitlindf  22909  pmatcollpw3lem  23014  pmatcollpw3fi1lem2  23018  cpmidpmatlem2  23102  cpmadumatpolylem1  23112  cayhamlem3  23118  cayhamlem4  23119  iscn  23466  iscnp  23468  cndis  23522  cnindis  23523  hausmapdom  23732  xkoptsub  23886  pt1hmeo  24038  flfval  24222  fcfval  24265  tmdgsum2  24328  symgtgp  24338  isucn  24509  ispsmet  24536  ismet  24555  isxmet  24556  imasdsf1olem  24605  elcncf  25123  metcld2  25541  elply2  26428  plyf  26430  elplyr  26433  plyeq0lem  26443  plyeq0  26444  plyaddlem  26448  plymullem  26449  dgrlem  26462  coeidlem  26470  ulmval  26623  ulmss  26640  ulmcn  26642  mtest  26647  pserulm  26665  isch2  31712  fmptco1f1o  33114  resf1o  33209  indf1ofs  33320  fedgmullem2  34148  smatrcl  34314  imambfm  34781  mbfmcnt  34787  isrrvv  34962  reprsuc  35131  reprinrn  35134  reprlt  35135  reprgt  35137  reprinfz1  35138  reprpmtf1o  35142  reprdifc  35143  circlevma  35158  deranglem  35753  indispconn  35821  prv1n  36018  knoppcnlem5  37202  knoppcnlem8  37205  fvopabf4g  38480  sdclem2  38500  sdclem1  38501  ismtyval  38558  rrncmslem  38590  aks6d1c2lem3  43000  aks6d1c5lem3  43011  aks6d1c5lem2  43012  sticksstones23  43043  mapfzcons  43569  mzpindd  43599  mzpsubst  43601  mzprename  43602  diophrw  43612  pw2f1ocnv  43886  ofoafg  44203  snelmap  45924  fvmap  46037  difmap  46045  mapssbi  46051  fourierdlem54  46996  fourierdlem111  47053  etransclem25  47095  qndenserrnbllem  47130  elhoi  47378  hoiprodcl2  47391  hoicvrrex  47392  ovnlecvr  47394  ovn0lem  47401  hsphoif  47412  hoidmvval  47413  hsphoival  47415  hoidmvle  47436  ovnhoilem1  47437  ovnhoilem2  47438  ovnlecvr2  47446  ovncvr2  47447  hoidifhspval2  47451  hoiqssbllem3  47460  hspmbllem2  47463  opnvonmbllem1  47468  nnsum3primesgbe  48716  nnsum4primesodd  48720  nnsum4primesoddALTV  48721  nnsum4primeseven  48724  nnsum4primesevenALTV  48725  isclintop  49130  funcringcsetcALTV2lem8  49220  funcringcsetclem8ALTV  49243  ofaddmndmap  49281  mapsnop  49282  zlmodzxzel  49293  linccl  49352  lincvalsc0  49359  lcoc0  49360  linc0scn0  49361  lincdifsn  49362  linc1  49363  lincsum  49367  lincscm  49368  lincscmcl  49370  lcoss  49374  lincext1  49392  lindslinindimp2lem2  49397  lindsrng01  49406  snlindsntorlem  49408  lincresunit1  49415  lincresunit3  49419  zlmodzxzldeplem1  49438  naryfvalel  49568  1arympt1fv  49577  1arymaptfo  49581  2arymaptf  49590  prelrrx2  49651  line2x  49692  line2y  49693  map0cor  49791