Theorem elmapd 8770

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2113  ⟶wf 6482  (class class class)co 7352   ↑_m cmap 8756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494  df-ov 7355  df-oprab 7356  df-mpo 7357  df-map 8758

This theorem is referenced by:  elmapdd  8771  mapfset  8780  mapfoss  8782  elmapssres  8797  elmapresaun  8810  mapsnd  8816  mapss  8819  ralxpmap  8826  mapen  9061  mapunen  9066  mapfienlem3  9298  mapfien  9299  cantnfs  9563  acni  9943  infmap2  10115  fin23lem32  10242  iundom2g  10438  wunf  10625  hashf1lem2  14365  prdsplusg  17364  prdsmulr  17365  prdsvsca  17366  elsetchom  17990  setcco  17992  elestrchom  18036  estrcco  18038  funcsetcestrclem7  18069  elefmndbas  18783  isga  19205  symgbasmap  19291  frlmvplusgvalc  21706  frlmplusgvalb  21708  frlmvscavalb  21709  evls1sca  22239  mamures  22313  mat1dimmul  22392  1mavmul  22464  mdetunilem9  22536  cnpdis  23209  xkopjcn  23572  indishmph  23714  tsmsxplem2  24070  rrx0el  25326  dchrfi  27194  ac6mapd  32608  elmaprd  32665  fcobij  32707  rmfsupp2  33212  elrgspnlem1  33216  elrgspnlem2  33217  elrgspnlem4  33219  elrgspnsubrunlem2  33222  elrgspnsubrun  33223  linds2eq  33353  elrspunidl  33400  lbsdiflsp0  33660  fedgmullem1  33663  fedgmullem2  33664  fedgmul  33665  zarcmplem  33915  mbfmcst  34293  1stmbfm  34294  2ndmbfm  34295  mbfmco  34298  sibfof  34374  satfv1lem  35427  ex-sategoelel  35486  ex-sategoelelomsuc  35491  aks6d1c1  42229  aks6d1c2lem4  42240  aks6d1c5lem0  42248  aks6d1c5  42252  aks6d1c6lem1  42283  aks6d1c6lem2  42284  frlmfielbas  42618  fsuppind  42708  fsuppssindlem2  42710  fsuppssind  42711  mhpind  42712  mapco2g  42831  cantnfub  43438  tfsconcatrev  43465  ofoafg  43471  ofoafo  43473  rfovcnvf1od  44121  fsovfd  44129  fsovcnvlem  44130  dssmapnvod  44137  clsk3nimkb  44157  ntrelmap  44242  clselmap  44244  k0004lem2  44265  elmapsnd  45325  mapss2  45326  unirnmap  45329  inmap  45330  difmapsn  45333  unirnmapsn  45335  fourierdlem14  46243  fourierdlem15  46244  fourierdlem81  46309  fourierdlem92  46320  rrnprjdstle  46423  subsaliuncllem  46479  hoidmvlelem3  46719  ovolval2lem  46765  ovolval4lem2  46772  ovolval5lem2  46775  ovnovollem1  46778  smfmullem4  46916  fprmappr  48469  el0ldep  48591  naryfvalelfv  48757  fv1arycl  48762  1arymaptf  48766  2arymaptfo  48779