Theorem elmapd 8880

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108  ⟶wf 6557  (class class class)co 7431   ↑_m cmap 8866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-map 8868

This theorem is referenced by:  elmapdd  8881  mapfset  8890  mapfoss  8892  elmapssres  8907  elmapresaun  8920  mapsnd  8926  mapss  8929  ralxpmap  8936  mapen  9181  mapunen  9186  f1finf1oOLD  9306  mapfienlem3  9447  mapfien  9448  cantnfs  9706  acni  10085  infmap2  10257  fin23lem32  10384  iundom2g  10580  wunf  10767  hashf1lem2  14495  prdsplusg  17503  prdsmulr  17504  prdsvsca  17505  elsetchom  18126  setcco  18128  elestrchom  18172  estrcco  18174  funcsetcestrclem7  18206  elefmndbas  18886  isga  19309  symgbasmap  19394  frlmvplusgvalc  21787  frlmplusgvalb  21789  frlmvscavalb  21790  evls1sca  22327  mamures  22401  mat1dimmul  22482  1mavmul  22554  mdetunilem9  22626  cnpdis  23301  xkopjcn  23664  indishmph  23806  tsmsxplem2  24162  rrx0el  25432  dchrfi  27299  ac6mapd  32635  elmaprd  32689  fcobij  32733  rmfsupp2  33242  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem4  33249  elrgspnsubrunlem2  33252  elrgspnsubrun  33253  linds2eq  33409  elrspunidl  33456  lbsdiflsp0  33677  fedgmullem1  33680  fedgmullem2  33681  fedgmul  33682  zarcmplem  33880  mbfmcst  34261  1stmbfm  34262  2ndmbfm  34263  mbfmco  34266  sibfof  34342  satfv1lem  35367  ex-sategoelel  35426  ex-sategoelelomsuc  35431  aks6d1c1  42117  aks6d1c2lem4  42128  aks6d1c5lem0  42136  aks6d1c5  42140  aks6d1c6lem1  42171  aks6d1c6lem2  42172  frlmfielbas  42510  fsuppind  42600  fsuppssindlem2  42602  fsuppssind  42603  mhpind  42604  mapco2g  42725  cantnfub  43334  tfsconcatrev  43361  ofoafg  43367  ofoafo  43369  rfovcnvf1od  44017  fsovfd  44025  fsovcnvlem  44026  dssmapnvod  44033  clsk3nimkb  44053  ntrelmap  44138  clselmap  44140  k0004lem2  44161  elmapsnd  45209  mapss2  45210  unirnmap  45213  inmap  45214  difmapsn  45217  unirnmapsn  45219  fourierdlem14  46136  fourierdlem15  46137  fourierdlem81  46202  fourierdlem92  46213  rrnprjdstle  46316  subsaliuncllem  46372  hoidmvlelem3  46612  ovolval2lem  46658  ovolval4lem2  46665  ovolval5lem2  46668  ovnovollem1  46671  smfmullem4  46809  fprmappr  48261  el0ldep  48383  naryfvalelfv  48553  fv1arycl  48558  1arymaptf  48562  2arymaptfo  48575