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

Theorem elmap 7750
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 (𝐹 ∈ (𝐴𝑚 𝐵) ↔ 𝐹:𝐵𝐴)

Proof of Theorem elmap
StepHypRef Expression
1 elmap.1 . 2 𝐴 ∈ V
2 elmap.2 . 2 𝐵 ∈ V
3 elmapg 7735 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐹 ∈ (𝐴𝑚 𝐵) ↔ 𝐹:𝐵𝐴))
41, 2, 3mp2an 703 1 (𝐹 ∈ (𝐴𝑚 𝐵) ↔ 𝐹:𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wcel 1976  Vcvv 3172  wf 5786  (class class class)co 6527  𝑚 cmap 7722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-map 7724
This theorem is referenced by:  mapval2  7751  fvmptmap  7758  mapsn  7763  mapsnconst  7767  mapsncnv  7768  xpmapenlem  7990  pwfseqlem3  9339  tskcard  9460  ingru  9494  rpnnen1lem1  11650  rpnnen1lem3  11651  rpnnen1lem4  11652  rpnnen1lem5  11653  rpnnen1lem1OLD  11656  rpnnen1lem3OLD  11657  rpnnen1lem4OLD  11658  rpnnen1lem5OLD  11659  facmapnn  12892  prmreclem2  15408  1arith  15418  vdwlem6  15477  vdwlem7  15478  vdwlem8  15479  vdwlem9  15480  vdwlem11  15482  vdwlem13  15484  prmgapprmo  15553  isfunc  16296  isfuncd  16297  idfucl  16313  cofucl  16320  funcres2b  16329  wunfunc  16331  catcfuccl  16531  funcestrcsetclem9  16560  ismhm  17109  symgval  17571  dfrhm2  18489  isabv  18591  psrelbas  19149  psraddcl  19153  psrmulcllem  19157  psrvscacl  19163  psr0cl  19164  psrnegcl  19166  psr1cl  19172  subrgpsr  19189  mvrf  19194  mplmon  19233  mplcoe1  19235  coe1fval3  19348  00ply1bas  19380  ply1plusgfvi  19382  coe1z  19403  coe1mul2  19409  coe1tm  19413  pjdm  19818  pjfval2  19820  pnrmopn  20905  distgp  21661  indistgp  21662  elovolm  22995  elovolmr  22996  ovolmge0  22997  ovolgelb  23000  ovolunlem1a  23016  ovolunlem1  23017  ovoliunlem1  23022  ovoliunlem2  23023  ovolshftlem2  23030  ovolicc2  23042  ioombl1  23082  itg2seq  23260  coeeulem  23729  coeeq  23732  aannenlem1  23832  dvntaylp  23874  taylthlem1  23876  taylthlem2  23877  pserdvlem2  23931  lgamgulmlem6  24505  sqff1o  24653  isismt  25175  elee  25520  islno  26826  nmooval  26836  ajfval  26882  h2hcau  27054  h2hlm  27055  hcau  27259  hlimadd  27268  hhcms  27278  hlim0  27310  hhsscms  27354  pjmf1  27793  hosmval  27812  hommval  27813  hodmval  27814  hfsmval  27815  hfmmval  27816  elcnop  27934  ellnop  27935  elhmop  27950  hmopex  27952  nlfnval  27958  elcnfn  27959  ellnfn  27960  dmadjss  27964  dmadjop  27965  adjeu  27966  adjval  27967  hhcno  27981  hhcnf  27982  adjbdln  28160  isst  28290  ishst  28291  maprnin  28728  fpwrelmap  28730  fpwrelmapffs  28731  eulerpartleme  29586  eulerpartlemt  29594  eulerpartlemr  29597  eulerpartlemmf  29598  eulerpartlemgvv  29599  eulerpartlemgs2  29603  eulerpartlemn  29604  mrsubff  30497  mrsubrn  30498  msubff  30515  poimirlem3  32406  poimirlem4  32407  poimirlem17  32420  poimirlem20  32423  poimirlem24  32427  poimirlem25  32428  poimirlem29  32432  poimirlem30  32433  poimirlem31  32434  poimirlem32  32435  isrngohom  32758  islfl  33189  islpolN  35614  constmap  36118  mzpclall  36132  mzpf  36141  mzpindd  36151  mzpcompact2lem  36156  eldiophb  36162  mendring  36605  clsk1independent  37188  k0004lem3  37291  dvnprodlem3  38662  fourierdlem70  38893  fourierdlem102  38925  fourierdlem114  38937  etransclem35  38986  hoicvrrex  39270  ovnhoilem1  39315  ovnovollem2  39371  nnsum3primes4  40029  nnsum3primesprm  40031  ismgmhm  41595  aacllem  42339
  Copyright terms: Public domain W3C validator