Theorem elmapd 8817

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

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2141  ⟶wf 6513  (class class class)co 7392   ↑_m cmap 8803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-pow 5321  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-fv 6525  df-ov 7395  df-oprab 7396  df-mpo 7397  df-map 8805

This theorem is referenced by:  elmapdd  8818  mapfset  8827  mapfoss  8829  elmapssres  8844  elmapresaun  8858  mapsnd  8864  mapss  8867  ralxpmap  8874  mapen  9109  mapunen  9114  mapfienlem3  9350  mapfien  9351  cantnfs  9618  acni  9998  infmap2  10170  fin23lem32  10298  iundom2g  10494  wunf  10682  hashf1lem2  14466  prdsplusg  17470  prdsmulr  17471  prdsvsca  17472  elsetchom  18097  setcco  18099  elestrchom  18143  estrcco  18145  funcsetcestrclem7  18176  elefmndbas  18890  isga  19314  symgbasmap  19400  frlmvplusgvalc  21799  frlmplusgvalb  21801  frlmvscavalb  21802  evls1sca  22366  mamures  22437  mat1dimmul  22516  1mavmul  22588  mdetunilem9  22660  cnpdis  23333  xkopjcn  23696  indishmph  23838  tsmsxplem2  24194  rrx0el  25440  dchrfi  27296  ac6mapd  32775  elmaprd  32832  fcobij  32872  rmfsupp2  33379  elrgspnlem1  33384  elrgspnlem2  33385  elrgspnlem4  33387  elrgspnsubrunlem2  33390  elrgspnsubrun  33391  linds2eq  33528  elrspunidl  33575  lbsdiflsp0  33884  fedgmullem1  33887  fedgmullem2  33888  fedgmul  33889  zarcmplem  34139  mbfmcst  34517  1stmbfm  34518  2ndmbfm  34519  mbfmco  34522  sibfof  34598  satfv1lem  35676  ex-sategoelel  35735  ex-sategoelelomsuc  35740  aks6d1c1  42697  aks6d1c2lem4  42708  aks6d1c5lem0  42716  aks6d1c5  42720  aks6d1c6lem1  42751  aks6d1c6lem2  42752  frlmfielbas  43086  fsuppind  43136  fsuppssindlem2  43138  fsuppssind  43139  mhpind  43140  mapco2g  43259  cantnfub  43862  tfsconcatrev  43889  ofoafg  43895  ofoafo  43897  rfovcnvf1od  44544  fsovfd  44552  fsovcnvlem  44553  dssmapnvod  44560  clsk3nimkb  44580  ntrelmap  44665  clselmap  44667  k0004lem2  44688  elmapsnd  45745  mapss2  45746  unirnmap  45748  inmap  45749  difmapsn  45752  unirnmapsn  45754  fourierdlem14  46659  fourierdlem15  46660  fourierdlem81  46725  fourierdlem92  46736  rrnprjdstle  46839  subsaliuncllem  46895  hoidmvlelem3  47135  ovolval2lem  47181  ovolval4lem2  47188  ovolval5lem2  47191  ovnovollem1  47194  smfmullem4  47332  fprmappr  48931  el0ldep  49052  naryfvalelfv  49218  fv1arycl  49223  1arymaptf  49227  2arymaptfo  49240