Theorem elmapd 8843

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2145  ⟶wf 6533  (class class class)co 7417   ↑_m cmap 8830

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pow 5334  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-map 8832

This theorem is used by:  elmapdd  8844  elmaprdOLD  8854  mapfset  8855  mapfoss  8857  elmapssres  8877  elmapresaun  8891  mapsnd  8897  mapss  8900  ralxpmap  8907  mapen  9143  mapunen  9148  mapfienlem3  9381  mapfien  9382  cantnfs  9649  acni  10052  infmap2  10223  fin23lem32  10350  iundom2g  10552  wunf  10740  hashf1lem2  14525  prdsplusg  17549  prdsmulr  17550  prdsvsca  17551  elsetchom  18176  setcco  18178  elestrchom  18222  estrcco  18224  funcsetcestrclem7  18255  elefmndbas  18988  isga  19424  symgbasmap  19510  frlmvplusgvalc  21986  frlmplusgvalb  21988  frlmvscavalb  21989  evls1sca  22554  mamures  22625  mat1dimmul  22704  1mavmul  22776  mdetunilem9  22848  cnpdis  23524  xkopjcn  23888  indishmph  24030  tsmsxplem2  24386  rrx0el  25632  dchrfi  27499  ac6mapd  33104  fcobij  33199  rmfsupp2  33685  elrgspnlem1  33690  elrgspnlem2  33691  elrgspnlem4  33693  elrgspnsubrunlem2  33696  elrgspnsubrun  33697  linds2eq  33822  elrspunidl  33864  lbsdiflsp0  34144  fedgmullem1  34147  fedgmullem2  34148  fedgmul  34149  zarcmplem  34399  mbfmcst  34778  1stmbfm  34779  2ndmbfm  34780  mbfmco  34783  sibfof  34859  satfv1lem  35949  ex-sategoelel  36008  ex-sategoelelomsuc  36013  aks6d1c1  42990  aks6d1c2lem4  43001  aks6d1c5lem0  43009  aks6d1c5  43013  aks6d1c6lem1  43044  aks6d1c6lem2  43045  frlmfielbas  43396  fsuppind  43444  fsuppssindlem2  43446  fsuppssind  43447  mhpind  43448  mapco2g  43567  cantnfub  44170  tfsconcatrev  44197  ofoafg  44203  ofoafo  44205  rfovcnvf1od  44852  fsovfd  44860  fsovcnvlem  44861  dssmapnvod  44868  clsk3nimkb  44888  ntrelmap  44973  clselmap  44975  k0004lem2  44996  elmapsnd  46043  mapss2  46044  unirnmap  46046  inmap  46047  difmapsn  46050  unirnmapsn  46052  fourierdlem14  46957  fourierdlem15  46958  fourierdlem81  47023  fourierdlem92  47034  rrnprjdstle  47137  subsaliuncllem  47193  hoidmvlelem3  47433  ovolval2lem  47479  ovolval4lem2  47486  ovolval5lem2  47489  ovnovollem1  47492  smfmullem4  47630  fprmappr  49283  el0ldep  49404  naryfvalelfv  49570  fv1arycl  49575  1arymaptf  49579  2arymaptfo  49592