Theorem elmapd 8830

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2106  ⟶wf 6536  (class class class)co 7405   ↑_m cmap 8816

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  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 6492  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-map 8818

This theorem is referenced by:  elmapdd  8831  mapfset  8840  mapfoss  8842  elmapssres  8857  elmapresaun  8870  mapsnd  8876  mapss  8879  ralxpmap  8886  mapen  9137  mapunen  9142  f1finf1oOLD  9268  mapfienlem3  9398  mapfien  9399  cantnfs  9657  acni  10036  infmap2  10209  fin23lem32  10335  iundom2g  10531  wunf  10718  hashf1lem1OLD  14412  hashf1lem2  14413  prdsplusg  17400  prdsmulr  17401  prdsvsca  17402  elsetchom  18027  setcco  18029  elestrchom  18075  estrcco  18077  funcsetcestrclem7  18109  elefmndbas  18750  isga  19149  symgbasmap  19238  frlmvplusgvalc  21313  frlmplusgvalb  21315  frlmvscavalb  21316  evls1sca  21833  mamures  21883  mat1dimmul  21969  1mavmul  22041  mdetunilem9  22113  cnpdis  22788  xkopjcn  23151  indishmph  23293  tsmsxplem2  23649  rrx0el  24906  dchrfi  26747  fcobij  31934  rmfsupp2  32375  linds2eq  32485  elrspunidl  32534  lbsdiflsp0  32699  fedgmullem1  32702  fedgmullem2  32703  fedgmul  32704  zarcmplem  32849  mbfmcst  33246  1stmbfm  33247  2ndmbfm  33248  mbfmco  33251  sibfof  33327  satfv1lem  34341  ex-sategoelel  34400  ex-sategoelelomsuc  34405  frlmfielbas  41071  selvcllem5  41151  fsuppind  41159  fsuppssindlem2  41161  fsuppssind  41162  mhpind  41163  mapco2g  41437  cantnfub  42056  tfsconcatrev  42083  ofoafg  42089  ofoafo  42091  rfovcnvf1od  42740  fsovfd  42748  fsovcnvlem  42749  dssmapnvod  42756  clsk3nimkb  42776  ntrelmap  42861  clselmap  42863  k0004lem2  42884  elmapsnd  43888  mapss2  43889  unirnmap  43892  inmap  43893  difmapsn  43896  unirnmapsn  43898  dvnprodlem1  44648  fourierdlem14  44823  fourierdlem15  44824  fourierdlem81  44889  fourierdlem92  44900  rrnprjdstle  45003  subsaliuncllem  45059  hoidmvlelem3  45299  ovolval2lem  45345  ovolval4lem2  45352  ovolval5lem2  45355  ovnovollem1  45358  smfmullem4  45496  fprmappr  46974  el0ldep  47100  naryfvalelfv  47271  fv1arycl  47276  1arymaptf  47280  2arymaptfo  47293