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

Theorem elmapg 8781
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.
StepHypRef Expression
1 mapvalg 8778 . . 3 ((𝐴𝑉𝐵𝑊) → (𝐴m 𝐵) = {𝑔𝑔:𝐵𝐴})
21eleq2d 2820 . 2 ((𝐴𝑉𝐵𝑊) → (𝐶 ∈ (𝐴m 𝐵) ↔ 𝐶 ∈ {𝑔𝑔:𝐵𝐴}))
3 fex2 7871 . . . . 5 ((𝐶:𝐵𝐴𝐵𝑊𝐴𝑉) → 𝐶 ∈ V)
433com13 1125 . . . 4 ((𝐴𝑉𝐵𝑊𝐶:𝐵𝐴) → 𝐶 ∈ V)
543expia 1122 . . 3 ((𝐴𝑉𝐵𝑊) → (𝐶:𝐵𝐴𝐶 ∈ V))
6 feq1 6650 . . . 4 (𝑔 = 𝐶 → (𝑔:𝐵𝐴𝐶:𝐵𝐴))
76elab3g 3638 . . 3 ((𝐶:𝐵𝐴𝐶 ∈ V) → (𝐶 ∈ {𝑔𝑔:𝐵𝐴} ↔ 𝐶:𝐵𝐴))
85, 7syl 17 . 2 ((𝐴𝑉𝐵𝑊) → (𝐶 ∈ {𝑔𝑔:𝐵𝐴} ↔ 𝐶:𝐵𝐴))
92, 8bitrd 279 1 ((𝐴𝑉𝐵𝑊) → (𝐶 ∈ (𝐴m 𝐵) ↔ 𝐶:𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wcel 2107  {cab 2710  Vcvv 3444  wf 6493  (class class class)co 7358  m cmap 8768
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3446  df-sbc 3741  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-map 8770
This theorem is referenced by:  elmapd  8782  mapdm0  8783  elmapi  8790  elmap  8812  map0g  8825  fdiagfn  8831  ralxpmap  8837  ixpssmap2g  8868  snmapen  8985  pw2f1olem  9023  mapxpen  9090  fseqenlem1  9965  fseqdom  9967  infpwfien  10003  fin23lem17  10279  fin23lem39  10291  isf34lem6  10321  gruurn  10739  intgru  10755  grutsk1  10762  hashfacenOLD  14358  wrdval  14411  wrdnval  14439  vdwlem4  16861  vdwlem9  16866  vdwlem10  16867  vdwlem11  16868  vdwlem13  16870  vdw  16871  vdwnnlem1  16872  rami  16892  ramcl  16906  prmgaplcm  16937  pwselbasb  17375  funcestrcsetclem7  18039  funcestrcsetclem8  18040  fullestrcsetc  18044  funcsetcestrclem8  18055  funcsetcestrclem9  18056  fullsetcestrc  18059  gsummptnn0fz  19768  frlmbasf  21182  frlmsplit2  21195  uvcff  21213  psrbag  21335  evlsval2  21513  coe1fsupp  21601  gsummoncoe1  21691  evls1sca  21705  mndvcl  21756  mamucl  21764  mamuvs1  21768  mamuvs2  21769  matbas2d  21788  matecl  21790  mamumat1cl  21804  mattposcl  21818  tposmap  21822  mat1dimelbas  21836  mavmulcl  21912  mdetunilem9  21985  pmatcollpw3lem  22148  pmatcollpw3fi1lem2  22152  cpmidpmatlem2  22236  cpmadumatpolylem1  22246  cayhamlem3  22252  cayhamlem4  22253  iscn  22602  iscnp  22604  cndis  22658  cnindis  22659  hausmapdom  22867  xkoptsub  23021  pt1hmeo  23173  flfval  23357  fcfval  23400  tmdgsum2  23463  symgtgp  23473  isucn  23646  ispsmet  23673  ismet  23692  isxmet  23693  imasdsf1olem  23742  elcncf  24268  metcld2  24687  elply2  25573  plyf  25575  elplyr  25578  plyeq0lem  25587  plyeq0  25588  plyaddlem  25592  plymullem  25593  dgrlem  25606  coeidlem  25614  ulmval  25755  ulmss  25772  ulmcn  25774  mtest  25779  pserulm  25797  isch2  30207  fmptco1f1o  31593  resf1o  31694  ply1degltdimlem  32374  fedgmullem2  32382  smatrcl  32434  indf1ofs  32682  imambfm  32919  mbfmcnt  32925  isrrvv  33100  reprsuc  33285  reprinrn  33288  reprlt  33289  reprgt  33291  reprinfz1  33292  reprpmtf1o  33296  reprdifc  33297  circlevma  33312  deranglem  33817  indispconn  33885  prv1n  34082  knoppcnlem5  35006  knoppcnlem8  35009  curf  36102  matunitlindflem1  36120  matunitlindflem2  36121  matunitlindf  36122  fvopabf4g  36226  sdclem2  36247  sdclem1  36248  ismtyval  36305  rrncmslem  36337  evlsval3  40787  mapfzcons  41082  mzpindd  41112  mzpsubst  41114  mzprename  41115  diophrw  41125  pw2f1ocnv  41404  ofoafg  41713  snelmap  43380  fvmap  43506  difmap  43515  mapssbi  43521  fourierdlem54  44487  fourierdlem111  44544  etransclem25  44586  qndenserrnbllem  44621  elhoi  44869  hoiprodcl2  44882  hoicvrrex  44883  ovnlecvr  44885  ovn0lem  44892  hsphoif  44903  hoidmvval  44904  hsphoival  44906  hoidmvle  44927  ovnhoilem1  44928  ovnhoilem2  44929  ovnlecvr2  44937  ovncvr2  44938  hoidifhspval2  44942  hoiqssbllem3  44951  hspmbllem2  44954  opnvonmbllem1  44959  nnsum3primesgbe  46070  nnsum4primesodd  46074  nnsum4primesoddALTV  46075  nnsum4primeseven  46078  nnsum4primesevenALTV  46079  isclintop  46227  isrnghm  46276  rnghmsscmap2  46357  rnghmsscmap  46358  funcrngcsetc  46382  funcrngcsetcALT  46383  rhmsscmap2  46403  rhmsscmap  46404  funcringcsetc  46419  funcringcsetcALTV2lem8  46427  funcringcsetclem8ALTV  46450  ofaddmndmap  46505  mapsnop  46506  zlmodzxzel  46517  linccl  46581  lincvalsc0  46588  lcoc0  46589  linc0scn0  46590  lincdifsn  46591  linc1  46592  lincsum  46596  lincscm  46597  lincscmcl  46599  lcoss  46603  lincext1  46621  lindslinindimp2lem2  46626  lindsrng01  46635  snlindsntorlem  46637  lincresunit1  46644  lincresunit3  46648  zlmodzxzldeplem1  46667  naryfvalel  46802  1arympt1fv  46811  1arymaptfo  46815  2arymaptf  46824  prelrrx2  46885  line2x  46926  line2y  46927  map0cor  47007
  Copyright terms: Public domain W3C validator