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

Theorem elmap 8121
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 8105 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐹 ∈ (𝐴𝑚 𝐵) ↔ 𝐹:𝐵𝐴))
41, 2, 3mp2an 675 1 (𝐹 ∈ (𝐴𝑚 𝐵) ↔ 𝐹:𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wcel 2156  Vcvv 3391  wf 6097  (class class class)co 6874  𝑚 cmap 8092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-fv 6109  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-map 8094
This theorem is referenced by:  mapval2  8122  fvmptmap  8129  mapsnconst  8140  mapsncnv  8141  xpmapenlem  8366  pwfseqlem3  9767  tskcard  9888  ingru  9922  rpnnen1lem1  12034  rpnnen1lem3  12035  rpnnen1lem4  12036  rpnnen1lem5  12037  facmapnn  13292  prmreclem2  15838  1arith  15848  vdwlem6  15907  vdwlem7  15908  vdwlem8  15909  vdwlem9  15910  vdwlem11  15912  vdwlem13  15914  prmgapprmo  15983  isfunc  16728  isfuncd  16729  idfucl  16745  cofucl  16752  funcres2b  16761  wunfunc  16763  catcfuccl  16963  funcestrcsetclem9  16993  ismhm  17542  symgval  18000  dfrhm2  18921  isabv  19023  psrelbas  19588  psraddcl  19592  psrmulcllem  19596  psrvscacl  19602  psr0cl  19603  psrnegcl  19605  psr1cl  19611  subrgpsr  19628  mvrf  19633  mplmon  19672  mplcoe1  19674  coe1fval3  19786  00ply1bas  19818  ply1plusgfvi  19820  coe1z  19841  coe1mul2  19847  coe1tm  19851  pjdm  20261  pjfval2  20263  pnrmopn  21361  distgp  22116  indistgp  22117  elovolmlem  23455  itg2seq  23723  coeeulem  24194  coeeq  24197  aannenlem1  24297  dvntaylp  24339  taylthlem1  24341  taylthlem2  24342  pserdvlem2  24396  lgamgulmlem6  24974  sqff1o  25122  isismt  25643  elee  25988  islno  27936  nmooval  27946  ajfval  27992  h2hcau  28164  h2hlm  28165  hcau  28369  hlimadd  28378  hhcms  28388  hlim0  28420  hhsscms  28464  pjmf1  28903  hosmval  28922  hommval  28923  hodmval  28924  hfsmval  28925  hfmmval  28926  elcnop  29044  ellnop  29045  elhmop  29060  hmopex  29062  nlfnval  29068  elcnfn  29069  ellnfn  29070  dmadjss  29074  dmadjop  29075  adjeu  29076  adjval  29077  hhcno  29091  hhcnf  29092  adjbdln  29270  isst  29400  ishst  29401  maprnin  29833  fpwrelmap  29835  fpwrelmapffs  29836  eulerpartleme  30750  eulerpartlemt  30758  eulerpartlemr  30761  eulerpartlemmf  30762  eulerpartlemgvv  30763  eulerpartlemgs2  30767  eulerpartlemn  30768  reprinfz1  31025  breprexplemb  31034  breprexpnat  31037  vtsval  31040  circlemethnat  31044  circlemethhgt  31046  mrsubff  31732  mrsubrn  31733  msubff  31750  poimirlem3  33725  poimirlem4  33726  poimirlem17  33739  poimirlem20  33742  poimirlem24  33746  poimirlem25  33747  poimirlem29  33751  poimirlem30  33752  poimirlem31  33753  poimirlem32  33754  isrngohom  34075  islfl  34840  islpolN  37264  constmap  37778  mzpclall  37792  mzpf  37801  mzpindd  37811  mzpcompact2lem  37816  eldiophb  37822  mendring  38263  clsk1independent  38844  k0004lem3  38947  dvnprodlem3  40643  fourierdlem70  40872  fourierdlem102  40904  fourierdlem114  40916  etransclem35  40965  hoicvrrex  41252  ovnhoilem1  41297  ovnovollem2  41353  nnsum3primes4  42251  nnsum3primesprm  42253  ismgmhm  42351  aacllem  43118
  Copyright terms: Public domain W3C validator