ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elmapg GIF version

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

Proof of Theorem elmapg
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 mapvalg 6482 . . 3 ((𝐴𝑉𝐵𝑊) → (𝐴𝑚 𝐵) = {𝑔𝑔:𝐵𝐴})
21eleq2d 2169 . 2 ((𝐴𝑉𝐵𝑊) → (𝐶 ∈ (𝐴𝑚 𝐵) ↔ 𝐶 ∈ {𝑔𝑔:𝐵𝐴}))
3 fex2 5227 . . . . 5 ((𝐶:𝐵𝐴𝐵𝑊𝐴𝑉) → 𝐶 ∈ V)
433com13 1154 . . . 4 ((𝐴𝑉𝐵𝑊𝐶:𝐵𝐴) → 𝐶 ∈ V)
543expia 1151 . . 3 ((𝐴𝑉𝐵𝑊) → (𝐶:𝐵𝐴𝐶 ∈ V))
6 feq1 5191 . . . 4 (𝑔 = 𝐶 → (𝑔:𝐵𝐴𝐶:𝐵𝐴))
76elab3g 2788 . . 3 ((𝐶:𝐵𝐴𝐶 ∈ V) → (𝐶 ∈ {𝑔𝑔:𝐵𝐴} ↔ 𝐶:𝐵𝐴))
85, 7syl 14 . 2 ((𝐴𝑉𝐵𝑊) → (𝐶 ∈ {𝑔𝑔:𝐵𝐴} ↔ 𝐶:𝐵𝐴))
92, 8bitrd 187 1 ((𝐴𝑉𝐵𝑊) → (𝐶 ∈ (𝐴𝑚 𝐵) ↔ 𝐶:𝐵𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wcel 1448  {cab 2086  Vcvv 2641  wf 5055  (class class class)co 5706  𝑚 cmap 6472
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-13 1459  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-pow 4038  ax-pr 4069  ax-un 4293  ax-setind 4390
This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-fal 1305  df-nf 1405  df-sb 1704  df-eu 1963  df-mo 1964  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ne 2268  df-ral 2380  df-rex 2381  df-v 2643  df-sbc 2863  df-dif 3023  df-un 3025  df-in 3027  df-ss 3034  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-br 3876  df-opab 3930  df-id 4153  df-xp 4483  df-rel 4484  df-cnv 4485  df-co 4486  df-dm 4487  df-rn 4488  df-iota 5024  df-fun 5061  df-fn 5062  df-f 5063  df-fv 5067  df-ov 5709  df-oprab 5710  df-mpo 5711  df-map 6474
This theorem is referenced by:  elmapd  6486  mapdm0  6487  elmapi  6494  elmap  6501  map0e  6510  map0g  6512  fdiagfn  6516  ixpssmap2g  6551  map1  6636  mapxpen  6671  isomnimap  6921  enomnilem  6922  ismkvmap  6940  hashfacen  10420  iscn  12147  iscnp  12149  cndis  12191  ispsmet  12251  ismet  12272  isxmet  12273  elcncf  12473  nnsf  12783
  Copyright terms: Public domain W3C validator