Theorem elmapd 8836

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2104  ⟶wf 6538  (class class class)co 7411   ↑_m cmap 8822

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-map 8824

This theorem is referenced by:  elmapdd  8837  mapfset  8846  mapfoss  8848  elmapssres  8863  elmapresaun  8876  mapsnd  8882  mapss  8885  ralxpmap  8892  mapen  9143  mapunen  9148  f1finf1oOLD  9274  mapfienlem3  9404  mapfien  9405  cantnfs  9663  acni  10042  infmap2  10215  fin23lem32  10341  iundom2g  10537  wunf  10724  hashf1lem1OLD  14420  hashf1lem2  14421  prdsplusg  17408  prdsmulr  17409  prdsvsca  17410  elsetchom  18035  setcco  18037  elestrchom  18083  estrcco  18085  funcsetcestrclem7  18117  elefmndbas  18790  isga  19196  symgbasmap  19285  frlmvplusgvalc  21541  frlmplusgvalb  21543  frlmvscavalb  21544  evls1sca  22062  mamures  22112  mat1dimmul  22198  1mavmul  22270  mdetunilem9  22342  cnpdis  23017  xkopjcn  23380  indishmph  23522  tsmsxplem2  23878  rrx0el  25146  dchrfi  26994  fcobij  32214  rmfsupp2  32657  linds2eq  32771  elrspunidl  32820  lbsdiflsp0  32999  fedgmullem1  33002  fedgmullem2  33003  fedgmul  33004  zarcmplem  33159  mbfmcst  33556  1stmbfm  33557  2ndmbfm  33558  mbfmco  33561  sibfof  33637  satfv1lem  34651  ex-sategoelel  34710  ex-sategoelelomsuc  34715  frlmfielbas  41380  selvcllem5  41456  fsuppind  41464  fsuppssindlem2  41466  fsuppssind  41467  mhpind  41468  mapco2g  41754  cantnfub  42373  tfsconcatrev  42400  ofoafg  42406  ofoafo  42408  rfovcnvf1od  43057  fsovfd  43065  fsovcnvlem  43066  dssmapnvod  43073  clsk3nimkb  43093  ntrelmap  43178  clselmap  43180  k0004lem2  43201  elmapsnd  44201  mapss2  44202  unirnmap  44205  inmap  44206  difmapsn  44209  unirnmapsn  44211  dvnprodlem1  44960  fourierdlem14  45135  fourierdlem15  45136  fourierdlem81  45201  fourierdlem92  45212  rrnprjdstle  45315  subsaliuncllem  45371  hoidmvlelem3  45611  ovolval2lem  45657  ovolval4lem2  45664  ovolval5lem2  45667  ovnovollem1  45670  smfmullem4  45808  fprmappr  47109  el0ldep  47234  naryfvalelfv  47405  fv1arycl  47410  1arymaptf  47414  2arymaptfo  47427