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

Theorem elmapg 6967
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 6964 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  ^m  B
)  =  { g  |  g : B --> A } )
21eleq2d 2454 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( C  e.  ( A  ^m  B )  <-> 
C  e.  { g  |  g : B --> A } ) )
3 fex2 5543 . . . . 5  |-  ( ( C : B --> A  /\  B  e.  W  /\  A  e.  V )  ->  C  e.  _V )
433com13 1158 . . . 4  |-  ( ( A  e.  V  /\  B  e.  W  /\  C : B --> A )  ->  C  e.  _V )
543expia 1155 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( C : B --> A  ->  C  e.  _V ) )
6 feq1 5516 . . . 4  |-  ( g  =  C  ->  (
g : B --> A  <->  C : B
--> A ) )
76elab3g 3031 . . 3  |-  ( ( C : B --> A  ->  C  e.  _V )  ->  ( C  e.  {
g  |  g : B --> A }  <->  C : B
--> A ) )
85, 7syl 16 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( C  e.  {
g  |  g : B --> A }  <->  C : B
--> A ) )
92, 8bitrd 245 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 177    /\ wa 359    e. wcel 1717   {cab 2373   _Vcvv 2899   -->wf 5390  (class class class)co 6020    ^m cmap 6954
This theorem is referenced by:  elmapi  6974  elmap  6978  map0e  6987  map0g  6989  mapss  6992  fdiagfn  6993  ixpssmap2g  7027  map1  7121  pw2f1olem  7148  mapen  7207  mapxpen  7209  mapunen  7212  f1finf1o  7271  cantnfs  7554  mapfien  7586  fseqenlem1  7838  fseqdom  7840  acni  7859  infpwfien  7876  infmap2  8031  fin23lem17  8151  fin23lem32  8157  fin23lem39  8163  isf34lem6  8193  iundom2g  8348  wunf  8535  gruurn  8606  intgru  8622  grutsk1  8629  hashfacen  11630  hashf1lem1  11631  hashf1lem2  11632  wrdval  11657  vdwlem4  13279  vdwlem9  13284  vdwlem10  13285  vdwlem11  13286  vdwlem13  13288  vdw  13289  vdwnnlem1  13290  rami  13310  ramcl  13324  prdsplusg  13608  prdsmulr  13609  prdsvsca  13610  pwselbasb  13637  elsetchom  14163  setcco  14165  isga  14995  symgbas  15022  psrbag  16358  iscn  17221  iscnp  17223  cndis  17277  cnindis  17278  cnpdis  17279  hausmapdom  17484  xkoptsub  17607  xkopjcn  17609  indishmph  17751  pt1hmeo  17759  flfval  17943  fcfval  17986  tmdgsum2  18047  symgtgp  18052  tsmsxplem2  18104  isucn  18229  ismet  18262  isxmet  18263  imasdsf1olem  18311  elcncf  18790  metcld2  19130  evlsval2  19808  elply2  19982  plyf  19984  elplyr  19987  plyeq0lem  19996  plyeq0  19997  plyaddlem  20001  plymullem  20002  dgrlem  20015  coeidlem  20023  ulmval  20163  ulmss  20180  ulmcn  20182  mtest  20187  pserulm  20205  dchrfi  20906  isch2  22574  indf1ofs  24219  mbfmcst  24403  1stmbfm  24404  2ndmbfm  24405  imambfm  24406  mbfmco  24408  mbfmcnt  24412  isrrvv  24480  deranglem  24631  indispcon  24700  fvopabf4g  26113  sdclem2  26137  sdclem1  26138  ismtyval  26200  rrncmslem  26232  ralxpmap  26433  mapco2g  26460  elmapssres  26462  mapfzcons  26463  mzpindd  26494  mzpsubst  26496  mzprename  26497  diophrw  26508  elmapresaun  26520  pw2f1ocnv  26799  frlmbas  26892  frlmbasf  26897  uvcff  26909  frlmsplit2  26912  elfilspd  26924  mndvcl  27115  mamucl  27125  mamudiagcl  27126  mamuvs1  27132  mamuvs2  27133
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-un 4641
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-sbc 3105  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-opab 4208  df-id 4439  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-iota 5358  df-fun 5396  df-fn 5397  df-f 5398  df-fv 5402  df-ov 6023  df-oprab 6024  df-mpt2 6025  df-map 6956
  Copyright terms: Public domain W3C validator