Theorem elmapd 8701

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2105  ⟶wf 6476  (class class class)co 7338   ↑_m cmap 8687

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-sbc 3728  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-br 5094  df-opab 5156  df-id 5519  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-fv 6488  df-ov 7341  df-oprab 7342  df-mpo 7343  df-map 8689

This theorem is referenced by:  mapfset  8710  mapfoss  8712  elmapssres  8727  elmapresaun  8740  mapsnd  8746  mapss  8749  ralxpmap  8756  mapen  9007  mapunen  9012  f1finf1oOLD  9138  mapfienlem3  9265  mapfien  9266  cantnfs  9524  acni  9903  infmap2  10076  fin23lem32  10202  iundom2g  10398  wunf  10585  hashf1lem1OLD  14270  hashf1lem2  14271  prdsplusg  17267  prdsmulr  17268  prdsvsca  17269  elsetchom  17894  setcco  17896  elestrchom  17942  estrcco  17944  funcsetcestrclem7  17976  elefmndbas  18609  isga  18994  symgbasmap  19081  frlmvplusgvalc  21081  frlmplusgvalb  21083  frlmvscavalb  21084  evls1sca  21596  mamures  21646  mat1dimmul  21732  1mavmul  21804  mdetunilem9  21876  cnpdis  22551  xkopjcn  22914  indishmph  23056  tsmsxplem2  23412  rrx0el  24669  dchrfi  26510  fcobij  31344  rmfsupp2  31779  linds2eq  31872  elrspunidl  31903  lbsdiflsp0  32005  fedgmullem1  32008  fedgmullem2  32009  fedgmul  32010  zarcmplem  32129  mbfmcst  32526  1stmbfm  32527  2ndmbfm  32528  mbfmco  32531  sibfof  32607  satfv1lem  33623  ex-sategoelel  33682  ex-sategoelelomsuc  33687  elmapdd  40519  selvval2lem4  40533  selvval2lem5  40534  frlmfielbas  40536  fsuppind  40590  fsuppssindlem2  40592  fsuppssind  40593  mhpind  40594  mapco2g  40849  ofoafg  41372  ofoafo  41374  rfovcnvf1od  41985  fsovfd  41993  fsovcnvlem  41994  dssmapnvod  42001  clsk3nimkb  42023  ntrelmap  42108  clselmap  42110  k0004lem2  42131  elmapsnd  43123  mapss2  43124  unirnmap  43127  inmap  43128  difmapsn  43131  unirnmapsn  43133  dvnprodlem1  43875  fourierdlem14  44050  fourierdlem15  44051  fourierdlem81  44116  fourierdlem92  44127  rrnprjdstle  44230  subsaliuncllem  44284  hoidmvlelem3  44524  ovolval2lem  44570  ovolval4lem2  44577  ovolval5lem2  44580  ovnovollem1  44583  smfmullem4  44721  fprmappr  46099  el0ldep  46225  naryfvalelfv  46396  fv1arycl  46401  1arymaptf  46405  2arymaptfo  46418