Theorem elmapg 8276

Description: Membership relation for set exponentiation. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.)

Assertion

Ref	Expression
elmapg	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Proof of Theorem elmapg

Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mapvalg 8273	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑𝑚 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2870	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7501	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1117	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1114	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6370	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3614	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 280	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑𝑚 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∈ wcel 2083  {cab 2777  Vcvv 3440  ⟶wf 6228  (class class class)co 7023   ↑_𝑚 cmap 8263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-sbc 3712  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-br 4969  df-opab 5031  df-id 5355  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-fv 6240  df-ov 7026  df-oprab 7027  df-mpo 7028  df-map 8265

This theorem is referenced by:  elmapd  8277  mapdm0  8278  elmapi  8285  elmap  8292  map0g  8305  fdiagfn  8310  ralxpmap  8316  ixpssmap2g  8346  snmapen  8445  pw2f1olem  8475  mapxpen  8537  fseqenlem1  9303  fseqdom  9305  infpwfien  9341  fin23lem17  9613  fin23lem39  9625  isf34lem6  9655  gruurn  10073  intgru  10089  grutsk1  10096  hashfacen  13664  wrdval  13714  wrdnval  13746  vdwlem4  16153  vdwlem9  16158  vdwlem10  16159  vdwlem11  16160  vdwlem13  16162  vdw  16163  vdwnnlem1  16164  rami  16184  ramcl  16198  prmgaplcm  16229  pwselbasb  16594  funcestrcsetclem7  17229  funcestrcsetclem8  17230  fullestrcsetc  17234  funcsetcestrclem8  17245  funcsetcestrclem9  17246  fullsetcestrc  17249  symgbas  18243  gsummptnn0fz  18827  psrbag  19836  evlsval2  19991  coe1fsupp  20069  gsummoncoe1  20159  evls1sca  20173  frlmbasf  20590  frlmsplit2  20603  uvcff  20621  mndvcl  20688  mamucl  20698  mamuvs1  20702  mamuvs2  20703  matbas2d  20720  matecl  20722  mamumat1cl  20736  mattposcl  20750  tposmap  20754  mat1dimelbas  20768  mavmulcl  20844  mdetunilem9  20917  pmatcollpw3lem  21079  pmatcollpw3fi1lem2  21083  cpmidpmatlem2  21167  cpmadumatpolylem1  21177  cayhamlem3  21183  cayhamlem4  21184  iscn  21531  iscnp  21533  cndis  21587  cnindis  21588  hausmapdom  21796  xkoptsub  21950  pt1hmeo  22102  flfval  22286  fcfval  22329  tmdgsum2  22392  symgtgp  22397  isucn  22574  ispsmet  22601  ismet  22620  isxmet  22621  imasdsf1olem  22670  elcncf  23184  metcld2  23597  elply2  24473  plyf  24475  elplyr  24478  plyeq0lem  24487  plyeq0  24488  plyaddlem  24492  plymullem  24493  dgrlem  24506  coeidlem  24514  ulmval  24655  ulmss  24672  ulmcn  24674  mtest  24679  pserulm  24697  isch2  28687  fmptco1f1o  30064  resf1o  30150  fedgmullem2  30626  smatrcl  30672  indf1ofs  30898  imambfm  31133  mbfmcnt  31139  isrrvv  31314  reprsuc  31499  reprinrn  31502  reprlt  31503  reprgt  31505  reprinfz1  31506  reprpmtf1o  31510  reprdifc  31511  circlevma  31526  deranglem  32023  indispconn  32091  prv1n  32288  knoppcnlem5  33447  knoppcnlem8  33450  curf  34422  matunitlindflem1  34440  matunitlindflem2  34441  matunitlindf  34442  fvopabf4g  34549  sdclem2  34570  sdclem1  34571  ismtyval  34631  rrncmslem  34663  mapfzcons  38819  mzpindd  38849  mzpsubst  38851  mzprename  38852  diophrw  38862  pw2f1ocnv  39140  snelmap  40906  fvmap  41021  difmap  41031  mapssbi  41037  fourierdlem54  42009  fourierdlem111  42066  etransclem25  42108  qndenserrnbllem  42143  elhoi  42388  hoiprodcl2  42401  hoicvrrex  42402  ovnlecvr  42404  ovn0lem  42411  hsphoif  42422  hoidmvval  42423  hsphoival  42425  hoidmvle  42446  ovnhoilem1  42447  ovnhoilem2  42448  ovnlecvr2  42456  ovncvr2  42457  hoidifhspval2  42461  hoiqssbllem3  42470  hspmbllem2  42473  opnvonmbllem1  42478  nnsum3primesgbe  43461  nnsum4primesodd  43465  nnsum4primesoddALTV  43466  nnsum4primeseven  43469  nnsum4primesevenALTV  43470  isclintop  43614  isrnghm  43663  rnghmsscmap2  43744  rnghmsscmap  43745  funcrngcsetc  43769  funcrngcsetcALT  43770  rhmsscmap2  43790  rhmsscmap  43791  funcringcsetc  43806  funcringcsetcALTV2lem8  43814  funcringcsetclem8ALTV  43837  ofaddmndmap  43892  mapsnop  43893  mapprop  43894  zlmodzxzel  43903  linccl  43971  lincvalsc0  43978  lcoc0  43979  linc0scn0  43980  lincdifsn  43981  linc1  43982  lincsum  43986  lincscm  43987  lincscmcl  43989  lcoss  43993  lincext1  44011  lindslinindimp2lem2  44016  lindsrng01  44025  snlindsntorlem  44027  lincresunit1  44034  lincresunit3  44038  zlmodzxzldeplem1  44057  prelrrx2  44203  line2x  44244  line2y  44245