Theorem elmapg 8788

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 8785	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑m 𝐵) = {𝑔 ∣ 𝑔:𝐵⟶𝐴})
2	1	eleq2d 2823	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴}))
3		fex2 7888	. . . . 5 ⊢ ((𝐶:𝐵⟶𝐴 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐶 ∈ V)
4	3	3com13 1125	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶:𝐵⟶𝐴) → 𝐶 ∈ V)
5	4	3expia 1122	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶:𝐵⟶𝐴 → 𝐶 ∈ V))
6		feq1 6648	. . . 4 ⊢ (𝑔 = 𝐶 → (𝑔:𝐵⟶𝐴 ↔ 𝐶:𝐵⟶𝐴))
7	6	elab3g 3642	. . 3 ⊢ ((𝐶:𝐵⟶𝐴 → 𝐶 ∈ V) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
8	5, 7	syl 17	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ {𝑔 ∣ 𝑔:𝐵⟶𝐴} ↔ 𝐶:𝐵⟶𝐴))
9	2, 8	bitrd 279	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  {cab 2715  Vcvv 3442  ⟶wf 6496  (class class class)co 7368   ↑_m cmap 8775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-map 8777

This theorem is referenced by:  elmapd  8789  mapdm0  8791  elmapi  8798  elmap  8821  map0g  8834  fdiagfn  8840  ralxpmap  8846  ixpssmap2g  8877  snmapen  8987  pw2f1olem  9021  mapxpen  9083  fseqenlem1  9946  fseqdom  9948  infpwfien  9984  fin23lem17  10260  fin23lem39  10272  isf34lem6  10302  gruurn  10721  intgru  10737  grutsk1  10744  wrdval  14451  wrdnval  14480  vdwlem4  16924  vdwlem9  16929  vdwlem10  16930  vdwlem11  16931  vdwlem13  16933  vdw  16934  vdwnnlem1  16935  rami  16955  ramcl  16969  prmgaplcm  17000  pwselbasb  17420  funcestrcsetclem7  18081  funcestrcsetclem8  18082  fullestrcsetc  18086  funcsetcestrclem8  18097  funcsetcestrclem9  18098  fullsetcestrc  18101  mndvcl  18734  gsummptnn0fz  19927  isrnghm  20389  rnghmsscmap2  20574  rnghmsscmap  20575  funcrngcsetc  20585  funcrngcsetcALT  20586  rhmsscmap2  20603  rhmsscmap  20604  funcringcsetc  20619  frlmbasf  21727  frlmsplit2  21740  uvcff  21758  psrbag  21885  evlsval2  22054  evlsval3  22056  coe1fsupp  22167  gsummoncoe1  22264  evls1sca  22279  mamucl  22357  mamuvs1  22361  mamuvs2  22362  matbas2d  22379  matecl  22381  mamumat1cl  22395  mattposcl  22409  tposmap  22413  mat1dimelbas  22427  mavmulcl  22503  mdetunilem9  22576  pmatcollpw3lem  22739  pmatcollpw3fi1lem2  22743  cpmidpmatlem2  22827  cpmadumatpolylem1  22837  cayhamlem3  22843  cayhamlem4  22844  iscn  23191  iscnp  23193  cndis  23247  cnindis  23248  hausmapdom  23456  xkoptsub  23610  pt1hmeo  23762  flfval  23946  fcfval  23989  tmdgsum2  24052  symgtgp  24062  isucn  24233  ispsmet  24260  ismet  24279  isxmet  24280  imasdsf1olem  24329  elcncf  24850  metcld2  25275  elply2  26169  plyf  26171  elplyr  26174  plyeq0lem  26183  plyeq0  26184  plyaddlem  26188  plymullem  26189  dgrlem  26202  coeidlem  26210  ulmval  26357  ulmss  26374  ulmcn  26376  mtest  26381  pserulm  26399  isch2  31310  fmptco1f1o  32722  resf1o  32819  indf1ofs  32958  fedgmullem2  33807  smatrcl  33973  imambfm  34439  mbfmcnt  34445  isrrvv  34620  reprsuc  34792  reprinrn  34795  reprlt  34796  reprgt  34798  reprinfz1  34799  reprpmtf1o  34803  reprdifc  34804  circlevma  34819  deranglem  35379  indispconn  35447  prv1n  35644  knoppcnlem5  36716  knoppcnlem8  36719  curf  37843  matunitlindflem1  37861  matunitlindflem2  37862  matunitlindf  37863  fvopabf4g  37967  sdclem2  37987  sdclem1  37988  ismtyval  38045  rrncmslem  38077  aks6d1c2lem3  42490  aks6d1c5lem3  42501  aks6d1c5lem2  42502  sticksstones23  42533  mapfzcons  43067  mzpindd  43097  mzpsubst  43099  mzprename  43100  diophrw  43110  pw2f1ocnv  43388  ofoafg  43705  snelmap  45436  fvmap  45550  difmap  45559  mapssbi  45565  fourierdlem54  46512  fourierdlem111  46569  etransclem25  46611  qndenserrnbllem  46646  elhoi  46894  hoiprodcl2  46907  hoicvrrex  46908  ovnlecvr  46910  ovn0lem  46917  hsphoif  46928  hoidmvval  46929  hsphoival  46931  hoidmvle  46952  ovnhoilem1  46953  ovnhoilem2  46954  ovnlecvr2  46962  ovncvr2  46963  hoidifhspval2  46967  hoiqssbllem3  46976  hspmbllem2  46979  opnvonmbllem1  46984  nnsum3primesgbe  48146  nnsum4primesodd  48150  nnsum4primesoddALTV  48151  nnsum4primeseven  48154  nnsum4primesevenALTV  48155  isclintop  48561  funcringcsetcALTV2lem8  48651  funcringcsetclem8ALTV  48674  ofaddmndmap  48697  mapsnop  48698  zlmodzxzel  48709  linccl  48768  lincvalsc0  48775  lcoc0  48776  linc0scn0  48777  lincdifsn  48778  linc1  48779  lincsum  48783  lincscm  48784  lincscmcl  48786  lcoss  48790  lincext1  48808  lindslinindimp2lem2  48813  lindsrng01  48822  snlindsntorlem  48824  lincresunit1  48831  lincresunit3  48835  zlmodzxzldeplem1  48854  naryfvalel  48984  1arympt1fv  48993  1arymaptfo  48997  2arymaptf  49006  prelrrx2  49067  line2x  49108  line2y  49109  map0cor  49208