Theorem elmapd 8784

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

Syntax hints:   → wi 4   ↔ wb 207   ∈ wcel 2119  ⟶wf 6488  (class class class)co 7363   ↑_m cmap 8770

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-map 8772

This theorem is referenced by:  elmapdd  8785  mapfset  8794  mapfoss  8796  elmapssres  8811  elmapresaun  8825  mapsnd  8831  mapss  8834  ralxpmap  8841  mapen  9076  mapunen  9081  mapfienlem3  9317  mapfien  9318  cantnfs  9585  acni  9965  infmap2  10137  fin23lem32  10264  iundom2g  10460  wunf  10648  hashf1lem2  14416  prdsplusg  17419  prdsmulr  17420  prdsvsca  17421  elsetchom  18046  setcco  18048  elestrchom  18092  estrcco  18094  funcsetcestrclem7  18125  elefmndbas  18839  isga  19264  symgbasmap  19350  frlmvplusgvalc  21749  frlmplusgvalb  21751  frlmvscavalb  21752  evls1sca  22316  mamures  22387  mat1dimmul  22466  1mavmul  22538  mdetunilem9  22610  cnpdis  23283  xkopjcn  23646  indishmph  23788  tsmsxplem2  24144  rrx0el  25390  dchrfi  27243  ac6mapd  32722  elmaprd  32779  fcobij  32819  rmfsupp2  33326  elrgspnlem1  33330  elrgspnlem2  33331  elrgspnlem4  33333  elrgspnsubrunlem2  33336  elrgspnsubrun  33337  linds2eq  33471  elrspunidl  33518  lbsdiflsp0  33817  fedgmullem1  33820  fedgmullem2  33821  fedgmul  33822  zarcmplem  34072  mbfmcst  34450  1stmbfm  34451  2ndmbfm  34452  mbfmco  34455  sibfof  34531  satfv1lem  35597  ex-sategoelel  35656  ex-sategoelelomsuc  35661  aks6d1c1  42608  aks6d1c2lem4  42619  aks6d1c5lem0  42627  aks6d1c5  42631  aks6d1c6lem1  42662  aks6d1c6lem2  42663  frlmfielbas  42997  fsuppind  43047  fsuppssindlem2  43049  fsuppssind  43050  mhpind  43051  mapco2g  43170  cantnfub  43773  tfsconcatrev  43800  ofoafg  43806  ofoafo  43808  rfovcnvf1od  44455  fsovfd  44463  fsovcnvlem  44464  dssmapnvod  44471  clsk3nimkb  44491  ntrelmap  44576  clselmap  44578  k0004lem2  44599  elmapsnd  45657  mapss2  45658  unirnmap  45660  inmap  45661  difmapsn  45664  unirnmapsn  45666  fourierdlem14  46571  fourierdlem15  46572  fourierdlem81  46637  fourierdlem92  46648  rrnprjdstle  46751  subsaliuncllem  46807  hoidmvlelem3  47047  ovolval2lem  47093  ovolval4lem2  47100  ovolval5lem2  47103  ovnovollem1  47106  smfmullem4  47244  fprmappr  48843  el0ldep  48964  naryfvalelfv  49130  fv1arycl  49135  1arymaptf  49139  2arymaptfo  49152