MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elmapg Structured version   Visualization version   GIF version

Theorem elmapg 7912
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.
StepHypRef Expression
1 mapvalg 7909 . . 3 ((𝐴𝑉𝐵𝑊) → (𝐴𝑚 𝐵) = {𝑔𝑔:𝐵𝐴})
21eleq2d 2716 . 2 ((𝐴𝑉𝐵𝑊) → (𝐶 ∈ (𝐴𝑚 𝐵) ↔ 𝐶 ∈ {𝑔𝑔:𝐵𝐴}))
3 fex2 7163 . . . . 5 ((𝐶:𝐵𝐴𝐵𝑊𝐴𝑉) → 𝐶 ∈ V)
433com13 1289 . . . 4 ((𝐴𝑉𝐵𝑊𝐶:𝐵𝐴) → 𝐶 ∈ V)
543expia 1286 . . 3 ((𝐴𝑉𝐵𝑊) → (𝐶:𝐵𝐴𝐶 ∈ V))
6 feq1 6064 . . . 4 (𝑔 = 𝐶 → (𝑔:𝐵𝐴𝐶:𝐵𝐴))
76elab3g 3389 . . 3 ((𝐶:𝐵𝐴𝐶 ∈ V) → (𝐶 ∈ {𝑔𝑔:𝐵𝐴} ↔ 𝐶:𝐵𝐴))
85, 7syl 17 . 2 ((𝐴𝑉𝐵𝑊) → (𝐶 ∈ {𝑔𝑔:𝐵𝐴} ↔ 𝐶:𝐵𝐴))
92, 8bitrd 268 1 ((𝐴𝑉𝐵𝑊) → (𝐶 ∈ (𝐴𝑚 𝐵) ↔ 𝐶:𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wcel 2030  {cab 2637  Vcvv 3231  wf 5922  (class class class)co 6690  𝑚 cmap 7899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-map 7901
This theorem is referenced by:  elmapd  7913  mapdm0  7914  elmapi  7921  elmap  7928  map0e  7937  map0g  7939  fdiagfn  7943  ralxpmap  7949  ixpssmap2g  7979  map1  8077  pw2f1olem  8105  mapxpen  8167  fseqenlem1  8885  fseqdom  8887  infpwfien  8923  fin23lem17  9198  fin23lem39  9210  isf34lem6  9240  gruurn  9658  intgru  9674  grutsk1  9681  hashfacen  13276  wrdval  13340  wrdnval  13367  vdwlem4  15735  vdwlem9  15740  vdwlem10  15741  vdwlem11  15742  vdwlem13  15744  vdw  15745  vdwnnlem1  15746  rami  15766  ramcl  15780  prmgaplcm  15811  pwselbasb  16195  elestrchom  16815  estrcco  16817  funcestrcsetclem7  16833  funcestrcsetclem8  16834  fullestrcsetc  16838  funcsetcestrclem7  16848  funcsetcestrclem8  16849  funcsetcestrclem9  16850  fullsetcestrc  16853  symgbas  17846  gsummptnn0fz  18428  psrbag  19412  evlsval2  19568  coe1fsupp  19632  gsummoncoe1  19722  evls1sca  19736  frlmbasf  20152  frlmsplit2  20160  uvcff  20178  mndvcl  20245  mamucl  20255  mamuvs1  20259  mamuvs2  20260  matbas2d  20277  matecl  20279  mamumat1cl  20293  mattposcl  20307  tposmap  20311  mat1dimelbas  20325  mavmulcl  20401  mdetunilem9  20474  pmatcollpw3lem  20636  pmatcollpw3fi1lem2  20640  cpmidpmatlem2  20724  cpmadumatpolylem1  20734  cayhamlem3  20740  cayhamlem4  20741  iscn  21087  iscnp  21089  cndis  21143  cnindis  21144  hausmapdom  21351  xkoptsub  21505  pt1hmeo  21657  flfval  21841  fcfval  21884  tmdgsum2  21947  symgtgp  21952  isucn  22129  ispsmet  22156  ismet  22175  isxmet  22176  imasdsf1olem  22225  elcncf  22739  metcld2  23151  elply2  23997  plyf  23999  elplyr  24002  plyeq0lem  24011  plyeq0  24012  plyaddlem  24016  plymullem  24017  dgrlem  24030  coeidlem  24038  ulmval  24179  ulmss  24196  ulmcn  24198  mtest  24203  pserulm  24221  isch2  28208  fmptco1f1o  29562  resf1o  29633  smatrcl  29990  indf1ofs  30216  imambfm  30452  mbfmcnt  30458  isrrvv  30633  reprsuc  30821  reprinrn  30824  reprlt  30825  reprgt  30827  reprinfz1  30828  reprpmtf1o  30832  reprdifc  30833  circlevma  30848  deranglem  31274  indispconn  31342  knoppcnlem5  32612  knoppcnlem8  32615  curf  33517  matunitlindflem1  33535  matunitlindflem2  33536  matunitlindf  33537  fvopabf4g  33645  sdclem2  33668  sdclem1  33669  ismtyval  33729  rrncmslem  33761  mapfzcons  37596  mzpindd  37626  mzpsubst  37628  mzprename  37629  diophrw  37639  pw2f1ocnv  37921  snelmap  39568  mapdm0OLD  39697  fvmap  39701  mapsnd  39702  difmap  39713  mapssbi  39719  fourierdlem54  40695  fourierdlem111  40752  etransclem25  40794  qndenserrnbllem  40832  elhoi  41077  hoiprodcl2  41090  hoicvrrex  41091  ovnlecvr  41093  ovn0lem  41100  hsphoif  41111  hoidmvval  41112  hsphoival  41114  hoidmvle  41135  ovnhoilem1  41136  ovnhoilem2  41137  ovnlecvr2  41145  ovncvr2  41146  hoidifhspval2  41150  hoiqssbllem3  41159  hspmbllem2  41162  opnvonmbllem1  41167  nnsum3primesgbe  42005  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  isclintop  42168  isrnghm  42217  rnghmsscmap2  42298  rnghmsscmap  42299  funcrngcsetc  42323  funcrngcsetcALT  42324  rhmsscmap2  42344  rhmsscmap  42345  funcringcsetc  42360  funcringcsetcALTV2lem8  42368  funcringcsetclem8ALTV  42391  ofaddmndmap  42447  mapsnop  42448  mapprop  42449  zlmodzxzel  42458  linccl  42528  lincvalsc0  42535  lcoc0  42536  linc0scn0  42537  lincdifsn  42538  linc1  42539  lincsum  42543  lincscm  42544  lincscmcl  42546  lcoss  42550  lincext1  42568  lindslinindimp2lem2  42573  lindsrng01  42582  snlindsntorlem  42584  lincresunit1  42591  lincresunit3  42595  zlmodzxzldeplem1  42614
  Copyright terms: Public domain W3C validator