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

Theorem elmap 8812
Description: Membership relation for set exponentiation. (Contributed by NM, 8-Dec-2003.)
Hypotheses
Ref Expression
elmap.1 𝐴 ∈ V
elmap.2 𝐵 ∈ V
Assertion
Ref Expression
elmap (𝐹 ∈ (𝐴m 𝐵) ↔ 𝐹:𝐵𝐴)

Proof of Theorem elmap
StepHypRef Expression
1 elmap.1 . 2 𝐴 ∈ V
2 elmap.2 . 2 𝐵 ∈ V
3 elmapg 8781 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐹 ∈ (𝐴m 𝐵) ↔ 𝐹:𝐵𝐴))
41, 2, 3mp2an 691 1 (𝐹 ∈ (𝐴m 𝐵) ↔ 𝐹:𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wcel 2107  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:  mapval2  8813  fvmptmap  8822  mapsnconst  8833  mapsncnv  8834  xpmapenlem  9091  pwfseqlem3  10601  tskcard  10722  ingru  10756  rpnnen1lem1  12908  rpnnen1lem3  12909  rpnnen1lem4  12910  rpnnen1lem5  12911  facmapnn  14191  prmreclem2  16794  1arith  16804  vdwlem6  16863  vdwlem7  16864  vdwlem8  16865  vdwlem9  16866  vdwlem11  16868  vdwlem13  16870  prmgapprmo  16939  isfunc  17755  isfuncd  17756  idfucl  17772  cofucl  17779  funcres2b  17788  wunfunc  17790  wunfuncOLD  17791  catcfuccl  18010  catcfucclOLD  18011  funcestrcsetclem9  18041  ismhm  18608  efmnd1bas  18708  smndex1ibas  18715  smndex1gbas  18717  dfrhm2  20155  isabv  20292  pjdm  21129  pjfval2  21131  psrelbas  21363  psraddcl  21367  psrmulcllem  21371  psrvscacl  21377  psr0cl  21378  psrnegcl  21380  psr1cl  21387  subrgpsr  21404  mvrf  21409  mplmon  21452  mplcoe1  21454  coe1fval3  21595  00ply1bas  21627  ply1plusgfvi  21629  coe1z  21650  coe1mul2  21656  coe1tm  21660  pnrmopn  22710  distgp  23466  indistgp  23467  ehl1eudis  24800  ehl2eudis  24802  elovolmlem  24854  itg2seq  25123  coeeulem  25601  coeeq  25604  aannenlem1  25704  dvntaylp  25746  taylthlem1  25748  taylthlem2  25749  pserdvlem2  25803  lgamgulmlem6  26399  sqff1o  26547  isismt  27518  elee  27885  islno  29737  nmooval  29747  ajfval  29793  h2hcau  29963  h2hlm  29964  hcau  30168  hlimadd  30177  hhcms  30187  hlim0  30219  hhsscms  30262  pjmf1  30700  hosmval  30719  hommval  30720  hodmval  30721  hfsmval  30722  hfmmval  30723  elcnop  30841  ellnop  30842  elhmop  30857  hmopex  30859  nlfnval  30865  elcnfn  30866  ellnfn  30867  dmadjss  30871  dmadjop  30872  adjeu  30873  adjval  30874  hhcno  30888  hhcnf  30889  adjbdln  31067  isst  31197  ishst  31198  maprnin  31695  fpwrelmap  31697  fpwrelmapffs  31698  ismnt  31892  mgcval  31896  fply1  32313  zarcmplem  32519  eulerpartleme  33020  eulerpartlemt  33028  eulerpartlemr  33031  eulerpartlemmf  33032  eulerpartlemgvv  33033  eulerpartlemgs2  33037  eulerpartlemn  33038  reprinfz1  33292  breprexplemb  33301  breprexpnat  33304  vtsval  33307  circlemethnat  33311  circlemethhgt  33313  ex-sategoelel12  34078  mrsubff  34163  mrsubrn  34164  msubff  34181  poimirlem3  36127  poimirlem4  36128  poimirlem17  36141  poimirlem20  36144  poimirlem24  36148  poimirlem25  36149  poimirlem29  36153  poimirlem30  36154  poimirlem31  36155  poimirlem32  36156  isrngohom  36470  islfl  37568  islpolN  39992  constmap  41079  mzpclall  41093  mzpf  41102  mzpindd  41112  mzpcompact2lem  41117  eldiophb  41123  mendring  41562  clsk1independent  42406  k0004lem3  42509  mnringmulrcld  42596  dvnprodlem3  44275  fourierdlem70  44503  fourierdlem102  44535  fourierdlem114  44547  etransclem35  44596  hoicvrrex  44883  ovnhoilem1  44928  ovnovollem2  44984  nnsum3primes4  46066  nnsum3primesprm  46068  ismgmhm  46163  rrx2xpref1o  46890  rrx2linesl  46915  line2  46924  line2x  46926  line2y  46927  funcf2lem  47124  aacllem  47334
  Copyright terms: Public domain W3C validator