Theorem elmapd 8787

Description: Deduction form of elmapg 8786. (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 8786	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))
4	1, 2, 3	syl2anc 585	1 ⊢ (𝜑 → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  ⟶wf 6494  (class class class)co 7367   ↑_m cmap 8773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-map 8775

This theorem is referenced by:  elmapdd  8788  mapfset  8797  mapfoss  8799  elmapssres  8814  elmapresaun  8828  mapsnd  8834  mapss  8837  ralxpmap  8844  mapen  9079  mapunen  9084  mapfienlem3  9320  mapfien  9321  cantnfs  9587  acni  9967  infmap2  10139  fin23lem32  10266  iundom2g  10462  wunf  10650  hashf1lem2  14418  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  elsetchom  18048  setcco  18050  elestrchom  18094  estrcco  18096  funcsetcestrclem7  18127  elefmndbas  18841  isga  19266  symgbasmap  19352  frlmvplusgvalc  21747  frlmplusgvalb  21749  frlmvscavalb  21750  evls1sca  22288  mamures  22362  mat1dimmul  22441  1mavmul  22513  mdetunilem9  22585  cnpdis  23258  xkopjcn  23621  indishmph  23763  tsmsxplem2  24119  rrx0el  25365  dchrfi  27218  ac6mapd  32696  elmaprd  32753  fcobij  32793  rmfsupp2  33299  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem4  33306  elrgspnsubrunlem2  33309  elrgspnsubrun  33310  linds2eq  33441  elrspunidl  33488  lbsdiflsp0  33770  fedgmullem1  33773  fedgmullem2  33774  fedgmul  33775  zarcmplem  34025  mbfmcst  34403  1stmbfm  34404  2ndmbfm  34405  mbfmco  34408  sibfof  34484  satfv1lem  35544  ex-sategoelel  35603  ex-sategoelelomsuc  35608  aks6d1c1  42555  aks6d1c2lem4  42566  aks6d1c5lem0  42574  aks6d1c5  42578  aks6d1c6lem1  42609  aks6d1c6lem2  42610  frlmfielbas  42945  fsuppind  43023  fsuppssindlem2  43025  fsuppssind  43026  mhpind  43027  mapco2g  43146  cantnfub  43749  tfsconcatrev  43776  ofoafg  43782  ofoafo  43784  rfovcnvf1od  44431  fsovfd  44439  fsovcnvlem  44440  dssmapnvod  44447  clsk3nimkb  44467  ntrelmap  44552  clselmap  44554  k0004lem2  44575  elmapsnd  45633  mapss2  45634  unirnmap  45637  inmap  45638  difmapsn  45641  unirnmapsn  45643  fourierdlem14  46549  fourierdlem15  46550  fourierdlem81  46615  fourierdlem92  46626  rrnprjdstle  46729  subsaliuncllem  46785  hoidmvlelem3  47025  ovolval2lem  47071  ovolval4lem2  47078  ovolval5lem2  47081  ovnovollem1  47084  smfmullem4  47222  fprmappr  48821  el0ldep  48942  naryfvalelfv  49108  fv1arycl  49113  1arymaptf  49117  2arymaptfo  49130