Theorem elmapd 8813

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  ⟶wf 6507  (class class class)co 7387   ↑_m cmap 8799

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-map 8801

This theorem is referenced by:  elmapdd  8814  mapfset  8823  mapfoss  8825  elmapssres  8840  elmapresaun  8853  mapsnd  8859  mapss  8862  ralxpmap  8869  mapen  9105  mapunen  9110  f1finf1oOLD  9217  mapfienlem3  9358  mapfien  9359  cantnfs  9619  acni  9998  infmap2  10170  fin23lem32  10297  iundom2g  10493  wunf  10680  hashf1lem2  14421  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  elsetchom  18043  setcco  18045  elestrchom  18089  estrcco  18091  funcsetcestrclem7  18122  elefmndbas  18800  isga  19223  symgbasmap  19307  frlmvplusgvalc  21676  frlmplusgvalb  21678  frlmvscavalb  21679  evls1sca  22210  mamures  22284  mat1dimmul  22363  1mavmul  22435  mdetunilem9  22507  cnpdis  23180  xkopjcn  23543  indishmph  23685  tsmsxplem2  24041  rrx0el  25298  dchrfi  27166  ac6mapd  32549  elmaprd  32603  fcobij  32645  rmfsupp2  33189  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnlem4  33196  elrgspnsubrunlem2  33199  elrgspnsubrun  33200  linds2eq  33352  elrspunidl  33399  lbsdiflsp0  33622  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  zarcmplem  33871  mbfmcst  34250  1stmbfm  34251  2ndmbfm  34252  mbfmco  34255  sibfof  34331  satfv1lem  35349  ex-sategoelel  35408  ex-sategoelelomsuc  35413  aks6d1c1  42104  aks6d1c2lem4  42115  aks6d1c5lem0  42123  aks6d1c5  42127  aks6d1c6lem1  42158  aks6d1c6lem2  42159  frlmfielbas  42488  fsuppind  42578  fsuppssindlem2  42580  fsuppssind  42581  mhpind  42582  mapco2g  42702  cantnfub  43310  tfsconcatrev  43337  ofoafg  43343  ofoafo  43345  rfovcnvf1od  43993  fsovfd  44001  fsovcnvlem  44002  dssmapnvod  44009  clsk3nimkb  44029  ntrelmap  44114  clselmap  44116  k0004lem2  44137  elmapsnd  45198  mapss2  45199  unirnmap  45202  inmap  45203  difmapsn  45206  unirnmapsn  45208  fourierdlem14  46119  fourierdlem15  46120  fourierdlem81  46185  fourierdlem92  46196  rrnprjdstle  46299  subsaliuncllem  46355  hoidmvlelem3  46595  ovolval2lem  46641  ovolval4lem2  46648  ovolval5lem2  46651  ovnovollem1  46654  smfmullem4  46792  fprmappr  48333  el0ldep  48455  naryfvalelfv  48621  fv1arycl  48626  1arymaptf  48630  2arymaptfo  48643