Theorem elmapd 8780

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  ⟶wf 6488  (class class class)co 7360   ↑_m cmap 8766

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 2709  ax-sep 5231  ax-pow 5302  ax-pr 5370  ax-un 7682

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-map 8768

This theorem is referenced by:  elmapdd  8781  mapfset  8790  mapfoss  8792  elmapssres  8807  elmapresaun  8821  mapsnd  8827  mapss  8830  ralxpmap  8837  mapen  9072  mapunen  9077  mapfienlem3  9313  mapfien  9314  cantnfs  9578  acni  9958  infmap2  10130  fin23lem32  10257  iundom2g  10453  wunf  10641  hashf1lem2  14409  prdsplusg  17412  prdsmulr  17413  prdsvsca  17414  elsetchom  18039  setcco  18041  elestrchom  18085  estrcco  18087  funcsetcestrclem7  18118  elefmndbas  18832  isga  19257  symgbasmap  19343  frlmvplusgvalc  21757  frlmplusgvalb  21759  frlmvscavalb  21760  evls1sca  22298  mamures  22372  mat1dimmul  22451  1mavmul  22523  mdetunilem9  22595  cnpdis  23268  xkopjcn  23631  indishmph  23773  tsmsxplem2  24129  rrx0el  25375  dchrfi  27232  ac6mapd  32711  elmaprd  32768  fcobij  32808  rmfsupp2  33314  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnlem4  33321  elrgspnsubrunlem2  33324  elrgspnsubrun  33325  linds2eq  33456  elrspunidl  33503  lbsdiflsp0  33786  fedgmullem1  33789  fedgmullem2  33790  fedgmul  33791  zarcmplem  34041  mbfmcst  34419  1stmbfm  34420  2ndmbfm  34421  mbfmco  34424  sibfof  34500  satfv1lem  35560  ex-sategoelel  35619  ex-sategoelelomsuc  35624  aks6d1c1  42569  aks6d1c2lem4  42580  aks6d1c5lem0  42588  aks6d1c5  42592  aks6d1c6lem1  42623  aks6d1c6lem2  42624  frlmfielbas  42959  fsuppind  43037  fsuppssindlem2  43039  fsuppssind  43040  mhpind  43041  mapco2g  43160  cantnfub  43767  tfsconcatrev  43794  ofoafg  43800  ofoafo  43802  rfovcnvf1od  44449  fsovfd  44457  fsovcnvlem  44458  dssmapnvod  44465  clsk3nimkb  44485  ntrelmap  44570  clselmap  44572  k0004lem2  44593  elmapsnd  45651  mapss2  45652  unirnmap  45655  inmap  45656  difmapsn  45659  unirnmapsn  45661  fourierdlem14  46567  fourierdlem15  46568  fourierdlem81  46633  fourierdlem92  46644  rrnprjdstle  46747  subsaliuncllem  46803  hoidmvlelem3  47043  ovolval2lem  47089  ovolval4lem2  47096  ovolval5lem2  47099  ovnovollem1  47102  smfmullem4  47240  fprmappr  48833  el0ldep  48954  naryfvalelfv  49120  fv1arycl  49125  1arymaptf  49129  2arymaptfo  49142