Theorem elmapd 8825

Description: Deduction form of elmapg 8824. (Contributed by BJ, 11-Apr-2020.)

Hypotheses

Ref	Expression
elmapd.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
elmapd.b	⊢ (𝜑 → 𝐵 ∈ 𝑊)

Assertion

Ref	Expression
elmapd	⊢ (𝜑 → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Proof of Theorem elmapd

Step	Hyp	Ref	Expression
1		elmapd.a	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		elmapd.b	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
3		elmapg 8824	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))
4	1, 2, 3	syl2anc 595	1 ⊢ (𝜑 → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2145  ⟶wf 6521  (class class class)co 7400   ↑_m cmap 8812

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-pow 5327  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-fv 6533  df-ov 7403  df-oprab 7404  df-mpo 7405  df-map 8814

This theorem is referenced by:  elmapdd  8826  mapfset  8835  mapfoss  8837  elmapssres  8852  elmapresaun  8866  mapsnd  8872  mapss  8875  ralxpmap  8882  mapen  9117  mapunen  9122  mapfienlem3  9355  mapfien  9356  cantnfs  9623  acni  10017  infmap2  10188  fin23lem32  10316  iundom2g  10512  wunf  10700  hashf1lem2  14483  prdsplusg  17501  prdsmulr  17502  prdsvsca  17503  elsetchom  18128  setcco  18130  elestrchom  18174  estrcco  18176  funcsetcestrclem7  18207  elefmndbas  18922  isga  19352  symgbasmap  19438  frlmvplusgvalc  21877  frlmplusgvalb  21879  frlmvscavalb  21880  evls1sca  22444  mamures  22515  mat1dimmul  22594  1mavmul  22666  mdetunilem9  22738  cnpdis  23411  xkopjcn  23774  indishmph  23916  tsmsxplem2  24272  rrx0el  25518  dchrfi  27377  ac6mapd  32880  elmaprd  32937  fcobij  32977  rmfsupp2  33470  elrgspnlem1  33475  elrgspnlem2  33476  elrgspnlem4  33478  elrgspnsubrunlem2  33481  elrgspnsubrun  33482  linds2eq  33610  elrspunidl  33652  lbsdiflsp0  33933  fedgmullem1  33936  fedgmullem2  33937  fedgmul  33938  zarcmplem  34188  mbfmcst  34566  1stmbfm  34567  2ndmbfm  34568  mbfmco  34571  sibfof  34647  satfv1lem  35725  ex-sategoelel  35784  ex-sategoelelomsuc  35789  aks6d1c1  42745  aks6d1c2lem4  42756  aks6d1c5lem0  42764  aks6d1c5  42768  aks6d1c6lem1  42799  aks6d1c6lem2  42800  frlmfielbas  43134  fsuppind  43184  fsuppssindlem2  43186  fsuppssind  43187  mhpind  43188  mapco2g  43307  cantnfub  43910  tfsconcatrev  43937  ofoafg  43943  ofoafo  43945  rfovcnvf1od  44592  fsovfd  44600  fsovcnvlem  44601  dssmapnvod  44608  clsk3nimkb  44628  ntrelmap  44713  clselmap  44715  k0004lem2  44736  elmapsnd  45779  mapss2  45780  unirnmap  45782  inmap  45783  difmapsn  45786  unirnmapsn  45788  fourierdlem14  46693  fourierdlem15  46694  fourierdlem81  46759  fourierdlem92  46770  rrnprjdstle  46873  subsaliuncllem  46929  hoidmvlelem3  47169  ovolval2lem  47215  ovolval4lem2  47222  ovolval5lem2  47225  ovnovollem1  47228  smfmullem4  47366  fprmappr  48976  el0ldep  49097  naryfvalelfv  49263  fv1arycl  49268  1arymaptf  49272  2arymaptfo  49285