Theorem elmapd 8838

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

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2143  ⟶wf 6534  (class class class)co 7412   ↑_m cmap 8825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7415  df-oprab 7416  df-mpo 7417  df-map 8827

This theorem is referenced by:  elmapdd  8839  mapfset  8848  mapfoss  8850  elmapssres  8865  elmapresaun  8879  mapsnd  8885  mapss  8888  ralxpmap  8895  mapen  9130  mapunen  9135  mapfienlem3  9368  mapfien  9369  cantnfs  9636  acni  10030  infmap2  10201  fin23lem32  10329  iundom2g  10525  wunf  10713  hashf1lem2  14495  prdsplusg  17512  prdsmulr  17513  prdsvsca  17514  elsetchom  18139  setcco  18141  elestrchom  18185  estrcco  18187  funcsetcestrclem7  18218  elefmndbas  18933  isga  19362  symgbasmap  19448  frlmvplusgvalc  21898  frlmplusgvalb  21900  frlmvscavalb  21901  evls1sca  22464  mamures  22535  mat1dimmul  22614  1mavmul  22686  mdetunilem9  22758  cnpdis  23431  xkopjcn  23794  indishmph  23936  tsmsxplem2  24292  rrx0el  25538  dchrfi  27397  ac6mapd  32946  elmaprd  33003  fcobij  33043  rmfsupp2  33535  elrgspnlem1  33540  elrgspnlem2  33541  elrgspnlem4  33543  elrgspnsubrunlem2  33546  elrgspnsubrun  33547  linds2eq  33672  elrspunidl  33714  lbsdiflsp0  33994  fedgmullem1  33997  fedgmullem2  33998  fedgmul  33999  zarcmplem  34249  mbfmcst  34627  1stmbfm  34628  2ndmbfm  34629  mbfmco  34632  sibfof  34708  satfv1lem  35832  ex-sategoelel  35891  ex-sategoelelomsuc  35896  aks6d1c1  42861  aks6d1c2lem4  42872  aks6d1c5lem0  42880  aks6d1c5  42884  aks6d1c6lem1  42915  aks6d1c6lem2  42916  frlmfielbas  43252  fsuppind  43302  fsuppssindlem2  43304  fsuppssind  43305  mhpind  43306  mapco2g  43425  cantnfub  44028  tfsconcatrev  44055  ofoafg  44061  ofoafo  44063  rfovcnvf1od  44710  fsovfd  44718  fsovcnvlem  44719  dssmapnvod  44726  clsk3nimkb  44746  ntrelmap  44831  clselmap  44833  k0004lem2  44854  elmapsnd  45901  mapss2  45902  unirnmap  45904  inmap  45905  difmapsn  45908  unirnmapsn  45910  fourierdlem14  46815  fourierdlem15  46816  fourierdlem81  46881  fourierdlem92  46892  rrnprjdstle  46995  subsaliuncllem  47051  hoidmvlelem3  47291  ovolval2lem  47337  ovolval4lem2  47344  ovolval5lem2  47347  ovnovollem1  47350  smfmullem4  47488  fprmappr  49102  el0ldep  49223  naryfvalelfv  49389  fv1arycl  49394  1arymaptf  49398  2arymaptfo  49411