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

Theorem elmap 6796
Description: Membership relation for set exponentiation. (Contributed by NM, 8-Dec-2003.)
Hypotheses
Ref Expression
elmap.1  |-  A  e. 
_V
elmap.2  |-  B  e. 
_V
Assertion
Ref Expression
elmap  |-  ( F  e.  ( A  ^m  B )  <->  F : B
--> A )

Proof of Theorem elmap
StepHypRef Expression
1 elmap.1 . 2  |-  A  e. 
_V
2 elmap.2 . 2  |-  B  e. 
_V
3 elmapg 6785 . 2  |-  ( ( A  e.  _V  /\  B  e.  _V )  ->  ( F  e.  ( A  ^m  B )  <-> 
F : B --> A ) )
41, 2, 3mp2an 653 1  |-  ( F  e.  ( A  ^m  B )  <->  F : B
--> A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    e. wcel 1684   _Vcvv 2788   -->wf 5251  (class class class)co 5858    ^m cmap 6772
This theorem is referenced by:  mapval2  6797  fvmptmap  6804  mapsn  6809  mapsnconst  6813  mapsncnv  6814  xpmapenlem  7028  pwfseqlem3  8282  tskcard  8403  ingru  8437  rpnnen1lem1  10342  rpnnen1lem3  10344  rpnnen1lem4  10345  rpnnen1lem5  10346  prmreclem2  12964  1arith  12974  vdwlem6  13033  vdwlem7  13034  vdwlem8  13035  vdwlem9  13036  vdwlem11  13038  vdwlem13  13040  isfunc  13738  isfuncd  13739  idfucl  13755  cofucl  13762  funcres2b  13771  wunfunc  13773  catcfuccl  13941  ismhm  14417  symgval  14771  dfrhm2  15498  isabv  15584  psrelbas  16125  psraddcl  16128  psrmulcllem  16132  psrvscacl  16138  psr0cl  16139  psrnegcl  16141  psr1cl  16147  subrgpsr  16163  mvrf  16169  mplmon  16207  mplcoe1  16209  coe1fval3  16289  00ply1bas  16318  ply1plusgfvi  16320  coe1z  16340  coe1mul2  16346  coe1tm  16349  pjdm  16607  pjfval2  16609  pnrmopn  17071  distgp  17782  indistgp  17783  elovolm  18834  elovolmr  18835  ovolmge0  18836  ovolgelb  18839  ovolunlem1a  18855  ovolunlem1  18856  ovoliunlem1  18861  ovoliunlem2  18862  ovolshftlem2  18869  ovolicc2  18881  ioombl1  18919  itg2seq  19097  coeeulem  19606  coeeq  19609  aannenlem1  19708  dvntaylp  19750  taylthlem1  19752  taylthlem2  19753  pserdvlem2  19804  sqff1o  20420  islno  21331  nmooval  21341  ajfval  21387  h2hcau  21559  h2hlm  21560  hcau  21763  hlimadd  21772  hhcms  21782  hlim0  21815  hhsscms  21856  pjmf1  22295  hosmval  22315  hommval  22316  hodmval  22317  hfsmval  22318  hfmmval  22319  elcnop  22437  ellnop  22438  elhmop  22453  hmopex  22455  nlfnval  22461  elcnfn  22462  ellnfn  22463  dmadjss  22467  dmadjop  22468  adjeu  22469  adjval  22470  hhcno  22484  hhcnf  22485  adjbdln  22663  isst  22793  ishst  22794  elee  24522  svli2  25484  cntrset  25602  claddrv  25647  claddrvr  25648  sigadd  25649  zernpl  25653  addcomv  25655  addidv2  25657  cnegvex2  25660  rnegvex2  25661  negveudr  25669  issubrv  25672  subclrvd  25674  clsmulcv  25682  clsmulrv  25683  fnmulcv  25684  mulone  25685  distsava  25689  divclrvd  25695  isfunb  25835  rocatval  25959  cmpidmor2  25969  phckle  26027  psckle  26028  fnckle  26045  fnckleb  26046  pgapspf  26052  isrngohom  26596  constmap  26788  mzpclall  26805  mzpf  26814  mzpindd  26824  mzpcompact2lem  26829  eldiophb  26836  mendrng  27500  islfl  29250  islpolN  31673
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