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

Theorem elmapg 8408
Description: Membership relation for set exponentiation. (Contributed by NM, 17-Oct-2006.) (Revised by Mario Carneiro, 15-Nov-2014.)
Assertion
Ref Expression
elmapg ((𝐴𝑉𝐵𝑊) → (𝐶 ∈ (𝐴m 𝐵) ↔ 𝐶:𝐵𝐴))

Proof of Theorem elmapg
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 mapvalg 8405 . . 3 ((𝐴𝑉𝐵𝑊) → (𝐴m 𝐵) = {𝑔𝑔:𝐵𝐴})
21eleq2d 2895 . 2 ((𝐴𝑉𝐵𝑊) → (𝐶 ∈ (𝐴m 𝐵) ↔ 𝐶 ∈ {𝑔𝑔:𝐵𝐴}))
3 fex2 7627 . . . . 5 ((𝐶:𝐵𝐴𝐵𝑊𝐴𝑉) → 𝐶 ∈ V)
433com13 1116 . . . 4 ((𝐴𝑉𝐵𝑊𝐶:𝐵𝐴) → 𝐶 ∈ V)
543expia 1113 . . 3 ((𝐴𝑉𝐵𝑊) → (𝐶:𝐵𝐴𝐶 ∈ V))
6 feq1 6488 . . . 4 (𝑔 = 𝐶 → (𝑔:𝐵𝐴𝐶:𝐵𝐴))
76elab3g 3670 . . 3 ((𝐶:𝐵𝐴𝐶 ∈ V) → (𝐶 ∈ {𝑔𝑔:𝐵𝐴} ↔ 𝐶:𝐵𝐴))
85, 7syl 17 . 2 ((𝐴𝑉𝐵𝑊) → (𝐶 ∈ {𝑔𝑔:𝐵𝐴} ↔ 𝐶:𝐵𝐴))
92, 8bitrd 280 1 ((𝐴𝑉𝐵𝑊) → (𝐶 ∈ (𝐴m 𝐵) ↔ 𝐶:𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wcel 2105  {cab 2796  Vcvv 3492  wf 6344  (class class class)co 7145  m cmap 8395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-map 8397
This theorem is referenced by:  elmapd  8409  mapdm0  8410  elmapi  8417  elmap  8424  map0g  8437  fdiagfn  8442  ralxpmap  8448  ixpssmap2g  8479  snmapen  8578  pw2f1olem  8609  mapxpen  8671  fseqenlem1  9438  fseqdom  9440  infpwfien  9476  fin23lem17  9748  fin23lem39  9760  isf34lem6  9790  gruurn  10208  intgru  10224  grutsk1  10231  hashfacen  13800  wrdval  13852  wrdnval  13884  vdwlem4  16308  vdwlem9  16313  vdwlem10  16314  vdwlem11  16315  vdwlem13  16317  vdw  16318  vdwnnlem1  16319  rami  16339  ramcl  16353  prmgaplcm  16384  pwselbasb  16749  funcestrcsetclem7  17384  funcestrcsetclem8  17385  fullestrcsetc  17389  funcsetcestrclem8  17400  funcsetcestrclem9  17401  fullsetcestrc  17404  symgbas  18436  gsummptnn0fz  19035  psrbag  20072  evlsval2  20228  coe1fsupp  20310  gsummoncoe1  20400  evls1sca  20414  frlmbasf  20832  frlmsplit2  20845  uvcff  20863  mndvcl  20930  mamucl  20938  mamuvs1  20942  mamuvs2  20943  matbas2d  20960  matecl  20962  mamumat1cl  20976  mattposcl  20990  tposmap  20994  mat1dimelbas  21008  mavmulcl  21084  mdetunilem9  21157  pmatcollpw3lem  21319  pmatcollpw3fi1lem2  21323  cpmidpmatlem2  21407  cpmadumatpolylem1  21417  cayhamlem3  21423  cayhamlem4  21424  iscn  21771  iscnp  21773  cndis  21827  cnindis  21828  hausmapdom  22036  xkoptsub  22190  pt1hmeo  22342  flfval  22526  fcfval  22569  tmdgsum2  22632  symgtgp  22637  isucn  22814  ispsmet  22841  ismet  22860  isxmet  22861  imasdsf1olem  22910  elcncf  23424  metcld2  23837  elply2  24713  plyf  24715  elplyr  24718  plyeq0lem  24727  plyeq0  24728  plyaddlem  24732  plymullem  24733  dgrlem  24746  coeidlem  24754  ulmval  24895  ulmss  24912  ulmcn  24914  mtest  24919  pserulm  24937  isch2  28927  fmptco1f1o  30306  resf1o  30392  fedgmullem2  30925  smatrcl  30960  indf1ofs  31184  imambfm  31419  mbfmcnt  31425  isrrvv  31600  reprsuc  31785  reprinrn  31788  reprlt  31789  reprgt  31791  reprinfz1  31792  reprpmtf1o  31796  reprdifc  31797  circlevma  31812  deranglem  32310  indispconn  32378  prv1n  32575  knoppcnlem5  33733  knoppcnlem8  33736  curf  34751  matunitlindflem1  34769  matunitlindflem2  34770  matunitlindf  34771  fvopabf4g  34877  sdclem2  34898  sdclem1  34899  ismtyval  34959  rrncmslem  34991  mapfzcons  39191  mzpindd  39221  mzpsubst  39223  mzprename  39224  diophrw  39234  pw2f1ocnv  39512  snelmap  41223  fvmap  41336  difmap  41346  mapssbi  41352  fourierdlem54  42322  fourierdlem111  42379  etransclem25  42421  qndenserrnbllem  42456  elhoi  42701  hoiprodcl2  42714  hoicvrrex  42715  ovnlecvr  42717  ovn0lem  42724  hsphoif  42735  hoidmvval  42736  hsphoival  42738  hoidmvle  42759  ovnhoilem1  42760  ovnhoilem2  42761  ovnlecvr2  42769  ovncvr2  42770  hoidifhspval2  42774  hoiqssbllem3  42783  hspmbllem2  42786  opnvonmbllem1  42791  nnsum3primesgbe  43834  nnsum4primesodd  43838  nnsum4primesoddALTV  43839  nnsum4primeseven  43842  nnsum4primesevenALTV  43843  isclintop  44042  isrnghm  44091  rnghmsscmap2  44172  rnghmsscmap  44173  funcrngcsetc  44197  funcrngcsetcALT  44198  rhmsscmap2  44218  rhmsscmap  44219  funcringcsetc  44234  funcringcsetcALTV2lem8  44242  funcringcsetclem8ALTV  44265  ofaddmndmap  44320  mapsnop  44321  mapprop  44322  zlmodzxzel  44331  linccl  44397  lincvalsc0  44404  lcoc0  44405  linc0scn0  44406  lincdifsn  44407  linc1  44408  lincsum  44412  lincscm  44413  lincscmcl  44415  lcoss  44419  lincext1  44437  lindslinindimp2lem2  44442  lindsrng01  44451  snlindsntorlem  44453  lincresunit1  44460  lincresunit3  44464  zlmodzxzldeplem1  44483  prelrrx2  44628  line2x  44669  line2y  44670
  Copyright terms: Public domain W3C validator