Theorem elmapd 8777

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2113  ⟶wf 6488  (class class class)co 7358   ↑_m cmap 8763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-map 8765

This theorem is referenced by:  elmapdd  8778  mapfset  8787  mapfoss  8789  elmapssres  8804  elmapresaun  8818  mapsnd  8824  mapss  8827  ralxpmap  8834  mapen  9069  mapunen  9074  mapfienlem3  9310  mapfien  9311  cantnfs  9575  acni  9955  infmap2  10127  fin23lem32  10254  iundom2g  10450  wunf  10638  hashf1lem2  14379  prdsplusg  17378  prdsmulr  17379  prdsvsca  17380  elsetchom  18005  setcco  18007  elestrchom  18051  estrcco  18053  funcsetcestrclem7  18084  elefmndbas  18798  isga  19220  symgbasmap  19306  frlmvplusgvalc  21722  frlmplusgvalb  21724  frlmvscavalb  21725  evls1sca  22267  mamures  22341  mat1dimmul  22420  1mavmul  22492  mdetunilem9  22564  cnpdis  23237  xkopjcn  23600  indishmph  23742  tsmsxplem2  24098  rrx0el  25354  dchrfi  27222  ac6mapd  32701  elmaprd  32759  fcobij  32799  rmfsupp2  33320  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem4  33327  elrgspnsubrunlem2  33330  elrgspnsubrun  33331  linds2eq  33462  elrspunidl  33509  lbsdiflsp0  33783  fedgmullem1  33786  fedgmullem2  33787  fedgmul  33788  zarcmplem  34038  mbfmcst  34416  1stmbfm  34417  2ndmbfm  34418  mbfmco  34421  sibfof  34497  satfv1lem  35556  ex-sategoelel  35615  ex-sategoelelomsuc  35620  aks6d1c1  42366  aks6d1c2lem4  42377  aks6d1c5lem0  42385  aks6d1c5  42389  aks6d1c6lem1  42420  aks6d1c6lem2  42421  frlmfielbas  42751  fsuppind  42829  fsuppssindlem2  42831  fsuppssind  42832  mhpind  42833  mapco2g  42952  cantnfub  43559  tfsconcatrev  43586  ofoafg  43592  ofoafo  43594  rfovcnvf1od  44241  fsovfd  44249  fsovcnvlem  44250  dssmapnvod  44257  clsk3nimkb  44277  ntrelmap  44362  clselmap  44364  k0004lem2  44385  elmapsnd  45444  mapss2  45445  unirnmap  45448  inmap  45449  difmapsn  45452  unirnmapsn  45454  fourierdlem14  46361  fourierdlem15  46362  fourierdlem81  46427  fourierdlem92  46438  rrnprjdstle  46541  subsaliuncllem  46597  hoidmvlelem3  46837  ovolval2lem  46883  ovolval4lem2  46890  ovolval5lem2  46893  ovnovollem1  46896  smfmullem4  47034  fprmappr  48587  el0ldep  48708  naryfvalelfv  48874  fv1arycl  48879  1arymaptf  48883  2arymaptfo  48896