Theorem elmapd 8861

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2099  ⟶wf 6542  (class class class)co 7416   ↑_m cmap 8847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-sbc 3776  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-br 5146  df-opab 5208  df-id 5572  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-fv 6554  df-ov 7419  df-oprab 7420  df-mpo 7421  df-map 8849

This theorem is referenced by:  elmapdd  8862  mapfset  8871  mapfoss  8873  elmapssres  8888  elmapresaun  8901  mapsnd  8907  mapss  8910  ralxpmap  8917  mapen  9171  mapunen  9176  f1finf1oOLD  9299  mapfienlem3  9443  mapfien  9444  cantnfs  9702  acni  10081  infmap2  10252  fin23lem32  10378  iundom2g  10574  wunf  10761  hashf1lem1OLD  14469  hashf1lem2  14470  prdsplusg  17468  prdsmulr  17469  prdsvsca  17470  elsetchom  18098  setcco  18100  elestrchom  18146  estrcco  18148  funcsetcestrclem7  18180  elefmndbas  18858  isga  19281  symgbasmap  19370  frlmvplusgvalc  21761  frlmplusgvalb  21763  frlmvscavalb  21764  evls1sca  22311  mamures  22385  mat1dimmul  22466  1mavmul  22538  mdetunilem9  22610  cnpdis  23285  xkopjcn  23648  indishmph  23790  tsmsxplem2  24146  rrx0el  25414  dchrfi  27281  fcobij  32636  rmfsupp2  33108  linds2eq  33262  elrspunidl  33309  lbsdiflsp0  33527  fedgmullem1  33530  fedgmullem2  33531  fedgmul  33532  zarcmplem  33709  mbfmcst  34106  1stmbfm  34107  2ndmbfm  34108  mbfmco  34111  sibfof  34187  satfv1lem  35203  ex-sategoelel  35262  ex-sategoelelomsuc  35267  aks6d1c1  41828  aks6d1c2lem4  41839  aks6d1c5lem0  41847  aks6d1c5  41851  aks6d1c6lem1  41882  aks6d1c6lem2  41883  frlmfielbas  42190  fsuppind  42280  fsuppssindlem2  42282  fsuppssind  42283  mhpind  42284  mapco2g  42408  cantnfub  43024  tfsconcatrev  43051  ofoafg  43057  ofoafo  43059  rfovcnvf1od  43708  fsovfd  43716  fsovcnvlem  43717  dssmapnvod  43724  clsk3nimkb  43744  ntrelmap  43829  clselmap  43831  k0004lem2  43852  elmapsnd  44847  mapss2  44848  unirnmap  44851  inmap  44852  difmapsn  44855  unirnmapsn  44857  dvnprodlem1  45603  fourierdlem14  45778  fourierdlem15  45779  fourierdlem81  45844  fourierdlem92  45855  rrnprjdstle  45958  subsaliuncllem  46014  hoidmvlelem3  46254  ovolval2lem  46300  ovolval4lem2  46307  ovolval5lem2  46310  ovnovollem1  46313  smfmullem4  46451  fprmappr  47760  el0ldep  47885  naryfvalelfv  48056  fv1arycl  48061  1arymaptf  48065  2arymaptfo  48078