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

Theorem elmapg 6785
Description: Membership relation for set exponentiation. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.)
Assertion
Ref Expression
elmapg  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( C  e.  ( A  ^m  B )  <-> 
C : B --> A ) )

Proof of Theorem elmapg
Dummy variable  g is distinct from all other variables.
StepHypRef Expression
1 mapvalg 6782 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  ^m  B
)  =  { g  |  g : B --> A } )
21eleq2d 2350 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( C  e.  ( A  ^m  B )  <-> 
C  e.  { g  |  g : B --> A } ) )
3 fex2 5401 . . . . 5  |-  ( ( C : B --> A  /\  B  e.  W  /\  A  e.  V )  ->  C  e.  _V )
433com13 1156 . . . 4  |-  ( ( A  e.  V  /\  B  e.  W  /\  C : B --> A )  ->  C  e.  _V )
543expia 1153 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( C : B --> A  ->  C  e.  _V ) )
6 feq1 5375 . . . 4  |-  ( g  =  C  ->  (
g : B --> A  <->  C : B
--> A ) )
76elab3g 2920 . . 3  |-  ( ( C : B --> A  ->  C  e.  _V )  ->  ( C  e.  {
g  |  g : B --> A }  <->  C : B
--> A ) )
85, 7syl 15 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( C  e.  {
g  |  g : B --> A }  <->  C : B
--> A ) )
92, 8bitrd 244 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( C  e.  ( A  ^m  B )  <-> 
C : B --> A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    e. wcel 1684   {cab 2269   _Vcvv 2788   -->wf 5251  (class class class)co 5858    ^m cmap 6772
This theorem is referenced by:  elmapi  6792  elmap  6796  map0e  6805  map0g  6807  mapss  6810  fdiagfn  6811  ixpssmap2g  6845  map1  6939  pw2f1olem  6966  mapen  7025  mapxpen  7027  mapunen  7030  f1finf1o  7086  cantnfs  7367  mapfien  7399  fseqenlem1  7651  fseqdom  7653  acni  7672  infpwfien  7689  infmap2  7844  fin23lem17  7964  fin23lem32  7970  fin23lem39  7976  isf34lem6  8006  iundom2g  8162  wunf  8349  gruurn  8420  intgru  8436  grutsk1  8443  hashfacen  11392  hashf1lem1  11393  hashf1lem2  11394  wrdval  11416  vdwlem4  13031  vdwlem9  13036  vdwlem10  13037  vdwlem11  13038  vdwlem13  13040  vdw  13041  vdwnnlem1  13042  rami  13062  ramcl  13076  prdsplusg  13358  prdsmulr  13359  prdsvsca  13360  pwselbasb  13387  elsetchom  13913  setcco  13915  isga  14745  symgbas  14772  psrbag  16112  iscn  16965  iscnp  16967  cndis  17019  cnindis  17020  cnpdis  17021  hausmapdom  17226  xkoptsub  17348  xkopjcn  17350  indishmph  17489  pt1hmeo  17497  flfval  17685  fcfval  17728  tmdgsum2  17779  symgtgp  17784  tsmsxplem2  17836  ismet  17888  isxmet  17889  imasdsf1olem  17937  elcncf  18393  metcld2  18732  evlsval2  19404  elply2  19578  plyf  19580  elplyr  19583  plyeq0lem  19592  plyeq0  19593  plyaddlem  19597  plymullem  19598  dgrlem  19611  coeidlem  19619  ulmval  19759  ulmss  19774  ulmcn  19776  mtest  19781  pserulm  19798  dchrfi  20494  isch2  21803  mbfmcst  23564  1stmbfm  23565  2ndmbfm  23566  imambfm  23567  mbfmco  23569  mbfmcnt  23573  indf1ofs  23609  isrrvv  23646  deranglem  23697  indispcon  23765  mappow  25089  ffvelrnb  25131  mapmapmap  25148  injsurinj  25149  mapdiscn  25527  mapudiscn  25528  islimrs3  25581  islimrs4  25582  claddrv  25647  sigadd  25649  addassv  25656  issubrv  25672  subclrvd  25674  clsmulcv  25682  clsmulrv  25683  fnmulcv  25684  distmlva  25688  isder  25707  propsrc  25868  fnctartar  25907  fnctartar2  25908  idcatfun  25941  cmpidmor3  25970  1iskle  25989  indcls2  25996  clscnc  26010  pgapspf2  26053  fvopabf4g  26386  sdclem2  26452  sdclem1  26453  ismtyval  26524  rrncmslem  26556  ralxpmap  26761  mapco2g  26790  elmapssres  26792  mapfzcons  26793  mzpindd  26824  mzpsubst  26826  mzprename  26827  diophrw  26838  elmapresaun  26850  pw2f1ocnv  27130  frlmbas  27223  frlmbasf  27228  uvcff  27240  frlmsplit2  27243  elfilspd  27255  mndvcl  27446  mamucl  27456  mamudiagcl  27457  mamuvs1  27463  mamuvs2  27464
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-map 6774
  Copyright terms: Public domain W3C validator