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

Theorem elmapg 6801
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 6798 . . 3  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( A  ^m  B
)  =  { g  |  g : B --> A } )
21eleq2d 2363 . 2  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( C  e.  ( A  ^m  B )  <-> 
C  e.  { g  |  g : B --> A } ) )
3 fex2 5417 . . . . 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 5391 . . . 4  |-  ( g  =  C  ->  (
g : B --> A  <->  C : B
--> A ) )
76elab3g 2933 . . 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 1696   {cab 2282   _Vcvv 2801   -->wf 5267  (class class class)co 5874    ^m cmap 6788
This theorem is referenced by:  elmapi  6808  elmap  6812  map0e  6821  map0g  6823  mapss  6826  fdiagfn  6827  ixpssmap2g  6861  map1  6955  pw2f1olem  6982  mapen  7041  mapxpen  7043  mapunen  7046  f1finf1o  7102  cantnfs  7383  mapfien  7415  fseqenlem1  7667  fseqdom  7669  acni  7688  infpwfien  7705  infmap2  7860  fin23lem17  7980  fin23lem32  7986  fin23lem39  7992  isf34lem6  8022  iundom2g  8178  wunf  8365  gruurn  8436  intgru  8452  grutsk1  8459  hashfacen  11408  hashf1lem1  11409  hashf1lem2  11410  wrdval  11432  vdwlem4  13047  vdwlem9  13052  vdwlem10  13053  vdwlem11  13054  vdwlem13  13056  vdw  13057  vdwnnlem1  13058  rami  13078  ramcl  13092  prdsplusg  13374  prdsmulr  13375  prdsvsca  13376  pwselbasb  13403  elsetchom  13929  setcco  13931  isga  14761  symgbas  14788  psrbag  16128  iscn  16981  iscnp  16983  cndis  17035  cnindis  17036  cnpdis  17037  hausmapdom  17242  xkoptsub  17364  xkopjcn  17366  indishmph  17505  pt1hmeo  17513  flfval  17701  fcfval  17744  tmdgsum2  17795  symgtgp  17800  tsmsxplem2  17852  ismet  17904  isxmet  17905  imasdsf1olem  17953  elcncf  18409  metcld2  18748  evlsval2  19420  elply2  19594  plyf  19596  elplyr  19599  plyeq0lem  19608  plyeq0  19609  plyaddlem  19613  plymullem  19614  dgrlem  19627  coeidlem  19635  ulmval  19775  ulmss  19790  ulmcn  19792  mtest  19797  pserulm  19814  dchrfi  20510  isch2  21819  mbfmcst  23579  1stmbfm  23580  2ndmbfm  23581  imambfm  23582  mbfmco  23584  mbfmcnt  23588  indf1ofs  23624  isrrvv  23661  deranglem  23712  indispcon  23780  mappow  25192  ffvelrnb  25234  mapmapmap  25251  injsurinj  25252  mapdiscn  25630  mapudiscn  25631  islimrs3  25684  islimrs4  25685  claddrv  25750  sigadd  25752  addassv  25759  issubrv  25775  subclrvd  25777  clsmulcv  25785  clsmulrv  25786  fnmulcv  25787  distmlva  25791  isder  25810  propsrc  25971  fnctartar  26010  fnctartar2  26011  idcatfun  26044  cmpidmor3  26073  1iskle  26092  indcls2  26099  clscnc  26113  pgapspf2  26156  fvopabf4g  26489  sdclem2  26555  sdclem1  26556  ismtyval  26627  rrncmslem  26659  ralxpmap  26864  mapco2g  26893  elmapssres  26895  mapfzcons  26896  mzpindd  26927  mzpsubst  26929  mzprename  26930  diophrw  26941  elmapresaun  26953  pw2f1ocnv  27233  frlmbas  27326  frlmbasf  27331  uvcff  27343  frlmsplit2  27346  elfilspd  27358  mndvcl  27549  mamucl  27559  mamudiagcl  27560  mamuvs1  27566  mamuvs2  27567
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-fv 5279  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-map 6790
  Copyright terms: Public domain W3C validator