Theorem elmapg 8824

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 8821	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑m 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2851	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7921	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1140	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1137	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6673	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3647	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 18	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 282	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2145  {cab 2743  Vcvv 3457  ⟶wf 6521  (class class class)co 7400   ↑_m cmap 8812

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-pow 5327  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-map 8814

This theorem is referenced by:  elmapd  8825  mapdm0  8827  elmapi  8834  elmap  8857  map0g  8870  fdiagfn  8876  ralxpmap  8882  ixpssmap2g  8913  snmapen  9023  pw2f1olem  9057  mapxpen  9119  fseqenlem1  9996  fseqdom  9998  infpwfien  10034  fin23lem17  10310  fin23lem39  10322  isf34lem6  10352  gruurn  10771  intgru  10787  grutsk1  10794  wrdval  14543  wrdnval  14572  vdwlem4  17034  vdwlem9  17039  vdwlem10  17040  vdwlem11  17041  vdwlem13  17043  vdw  17044  vdwnnlem1  17045  rami  17065  ramcl  17079  prmgaplcm  17110  pwselbasb  17531  funcestrcsetclem7  18192  funcestrcsetclem8  18193  fullestrcsetc  18197  funcsetcestrclem8  18208  funcsetcestrclem9  18209  fullsetcestrc  18212  mndvcl  18845  gsummptnn0fz  20047  isrnghm  20514  rnghmsscmap2  20705  rnghmsscmap  20706  funcrngcsetc  20716  funcrngcsetcALT  20717  rhmsscmap2  20734  rhmsscmap  20735  funcringcsetc  20750  frlmbasf  21870  frlmsplit2  21883  uvcff  21901  psrbag  22027  evlsval2  22198  evlsval3  22200  coe1fsupp  22334  gsummoncoe1  22429  evls1sca  22444  mamucl  22519  mamuvs1  22523  mamuvs2  22524  matbas2d  22541  matecl  22543  mamumat1cl  22557  mattposcl  22571  tposmap  22575  mat1dimelbas  22589  mavmulcl  22665  mdetunilem9  22738  pmatcollpw3lem  22901  pmatcollpw3fi1lem2  22905  cpmidpmatlem2  22989  cpmadumatpolylem1  22999  cayhamlem3  23005  cayhamlem4  23006  iscn  23353  iscnp  23355  cndis  23409  cnindis  23410  hausmapdom  23618  xkoptsub  23772  pt1hmeo  23924  flfval  24108  fcfval  24151  tmdgsum2  24214  symgtgp  24224  isucn  24395  ispsmet  24422  ismet  24441  isxmet  24442  imasdsf1olem  24491  elcncf  25009  metcld2  25427  elply2  26314  plyf  26316  elplyr  26319  plyeq0lem  26328  plyeq0  26329  plyaddlem  26333  plymullem  26334  dgrlem  26347  coeidlem  26355  ulmval  26501  ulmss  26518  ulmcn  26520  mtest  26525  pserulm  26543  isch2  31484  fmptco1f1o  32890  resf1o  32987  indf1ofs  33099  fedgmullem2  33937  smatrcl  34103  imambfm  34569  mbfmcnt  34575  isrrvv  34750  reprsuc  34919  reprinrn  34922  reprlt  34923  reprgt  34925  reprinfz1  34926  reprpmtf1o  34930  reprdifc  34931  circlevma  34946  deranglem  35529  indispconn  35597  prv1n  35794  knoppcnlem5  36948  knoppcnlem8  36951  curf  38109  matunitlindflem1  38127  matunitlindflem2  38128  matunitlindf  38129  fvopabf4g  38233  sdclem2  38253  sdclem1  38254  ismtyval  38311  rrncmslem  38343  aks6d1c2lem3  42755  aks6d1c5lem3  42766  aks6d1c5lem2  42767  sticksstones23  42798  mapfzcons  43309  mzpindd  43339  mzpsubst  43341  mzprename  43342  diophrw  43352  pw2f1ocnv  43626  ofoafg  43943  snelmap  45660  fvmap  45773  difmap  45781  mapssbi  45787  fourierdlem54  46732  fourierdlem111  46789  etransclem25  46831  qndenserrnbllem  46866  elhoi  47114  hoiprodcl2  47127  hoicvrrex  47128  ovnlecvr  47130  ovn0lem  47137  hsphoif  47148  hoidmvval  47149  hsphoival  47151  hoidmvle  47172  ovnhoilem1  47173  ovnhoilem2  47174  ovnlecvr2  47182  ovncvr2  47183  hoidifhspval2  47187  hoiqssbllem3  47196  hspmbllem2  47199  opnvonmbllem1  47204  nnsum3primesgbe  48412  nnsum4primesodd  48416  nnsum4primesoddALTV  48417  nnsum4primeseven  48420  nnsum4primesevenALTV  48421  isclintop  48827  funcringcsetcALTV2lem8  48917  funcringcsetclem8ALTV  48940  ofaddmndmap  48974  mapsnop  48975  zlmodzxzel  48986  linccl  49045  lincvalsc0  49052  lcoc0  49053  linc0scn0  49054  lincdifsn  49055  linc1  49056  lincsum  49060  lincscm  49061  lincscmcl  49063  lcoss  49067  lincext1  49085  lindslinindimp2lem2  49090  lindsrng01  49099  snlindsntorlem  49101  lincresunit1  49108  lincresunit3  49112  zlmodzxzldeplem1  49131  naryfvalel  49261  1arympt1fv  49270  1arymaptfo  49274  2arymaptf  49283  prelrrx2  49344  line2x  49385  line2y  49386  map0cor  49484