Theorem elmapg 8877

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2105  {cab 2711  Vcvv 3477  ⟶wf 6558  (class class class)co 7430   ↑_m cmap 8864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-map 8866

This theorem is referenced by:  elmapd  8878  mapdm0  8880  elmapi  8887  elmap  8909  map0g  8922  fdiagfn  8928  ralxpmap  8934  ixpssmap2g  8965  snmapen  9076  pw2f1olem  9114  mapxpen  9181  fseqenlem1  10061  fseqdom  10063  infpwfien  10099  fin23lem17  10375  fin23lem39  10387  isf34lem6  10417  gruurn  10835  intgru  10851  grutsk1  10858  wrdval  14551  wrdnval  14579  vdwlem4  17017  vdwlem9  17022  vdwlem10  17023  vdwlem11  17024  vdwlem13  17026  vdw  17027  vdwnnlem1  17028  rami  17048  ramcl  17062  prmgaplcm  17093  pwselbasb  17534  funcestrcsetclem7  18201  funcestrcsetclem8  18202  fullestrcsetc  18206  funcsetcestrclem8  18217  funcsetcestrclem9  18218  fullsetcestrc  18221  mndvcl  18822  gsummptnn0fz  20018  isrnghm  20457  rnghmsscmap2  20645  rnghmsscmap  20646  funcrngcsetc  20656  funcrngcsetcALT  20657  rhmsscmap2  20674  rhmsscmap  20675  funcringcsetc  20690  frlmbasf  21797  frlmsplit2  21810  uvcff  21828  psrbag  21954  evlsval2  22128  coe1fsupp  22231  gsummoncoe1  22327  evls1sca  22342  mamucl  22420  mamuvs1  22424  mamuvs2  22425  matbas2d  22444  matecl  22446  mamumat1cl  22460  mattposcl  22474  tposmap  22478  mat1dimelbas  22492  mavmulcl  22568  mdetunilem9  22641  pmatcollpw3lem  22804  pmatcollpw3fi1lem2  22808  cpmidpmatlem2  22892  cpmadumatpolylem1  22902  cayhamlem3  22908  cayhamlem4  22909  iscn  23258  iscnp  23260  cndis  23314  cnindis  23315  hausmapdom  23523  xkoptsub  23677  pt1hmeo  23829  flfval  24013  fcfval  24056  tmdgsum2  24119  symgtgp  24129  isucn  24302  ispsmet  24329  ismet  24348  isxmet  24349  imasdsf1olem  24398  elcncf  24928  metcld2  25354  elply2  26249  plyf  26251  elplyr  26254  plyeq0lem  26263  plyeq0  26264  plyaddlem  26268  plymullem  26269  dgrlem  26282  coeidlem  26290  ulmval  26437  ulmss  26454  ulmcn  26456  mtest  26461  pserulm  26479  isch2  31251  fmptco1f1o  32649  resf1o  32747  fedgmullem2  33657  smatrcl  33756  indf1ofs  34006  imambfm  34243  mbfmcnt  34249  isrrvv  34424  reprsuc  34608  reprinrn  34611  reprlt  34612  reprgt  34614  reprinfz1  34615  reprpmtf1o  34619  reprdifc  34620  circlevma  34635  deranglem  35150  indispconn  35218  prv1n  35415  knoppcnlem5  36479  knoppcnlem8  36482  curf  37584  matunitlindflem1  37602  matunitlindflem2  37603  matunitlindf  37604  fvopabf4g  37708  sdclem2  37728  sdclem1  37729  ismtyval  37786  rrncmslem  37818  aks6d1c2lem3  42107  aks6d1c5lem3  42118  aks6d1c5lem2  42119  sticksstones23  42150  evlsval3  42545  mapfzcons  42703  mzpindd  42733  mzpsubst  42735  mzprename  42736  diophrw  42746  pw2f1ocnv  43025  ofoafg  43343  snelmap  45021  fvmap  45140  difmap  45149  mapssbi  45155  fourierdlem54  46115  fourierdlem111  46172  etransclem25  46214  qndenserrnbllem  46249  elhoi  46497  hoiprodcl2  46510  hoicvrrex  46511  ovnlecvr  46513  ovn0lem  46520  hsphoif  46531  hoidmvval  46532  hsphoival  46534  hoidmvle  46555  ovnhoilem1  46556  ovnhoilem2  46557  ovnlecvr2  46565  ovncvr2  46566  hoidifhspval2  46570  hoiqssbllem3  46579  hspmbllem2  46582  opnvonmbllem1  46587  nnsum3primesgbe  47716  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  isclintop  48050  funcringcsetcALTV2lem8  48140  funcringcsetclem8ALTV  48163  ofaddmndmap  48187  mapsnop  48188  zlmodzxzel  48199  linccl  48259  lincvalsc0  48266  lcoc0  48267  linc0scn0  48268  lincdifsn  48269  linc1  48270  lincsum  48274  lincscm  48275  lincscmcl  48277  lcoss  48281  lincext1  48299  lindslinindimp2lem2  48304  lindsrng01  48313  snlindsntorlem  48315  lincresunit1  48322  lincresunit3  48326  zlmodzxzldeplem1  48345  naryfvalel  48479  1arympt1fv  48488  1arymaptfo  48492  2arymaptf  48501  prelrrx2  48562  line2x  48603  line2y  48604  map0cor  48684