Theorem elmapd 8789

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  ⟶wf 6496  (class class class)co 7368   ↑_m cmap 8775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-map 8777

This theorem is referenced by:  elmapdd  8790  mapfset  8799  mapfoss  8801  elmapssres  8816  elmapresaun  8830  mapsnd  8836  mapss  8839  ralxpmap  8846  mapen  9081  mapunen  9086  mapfienlem3  9322  mapfien  9323  cantnfs  9587  acni  9967  infmap2  10139  fin23lem32  10266  iundom2g  10462  wunf  10650  hashf1lem2  14391  prdsplusg  17390  prdsmulr  17391  prdsvsca  17392  elsetchom  18017  setcco  18019  elestrchom  18063  estrcco  18065  funcsetcestrclem7  18096  elefmndbas  18810  isga  19232  symgbasmap  19318  frlmvplusgvalc  21734  frlmplusgvalb  21736  frlmvscavalb  21737  evls1sca  22279  mamures  22353  mat1dimmul  22432  1mavmul  22504  mdetunilem9  22576  cnpdis  23249  xkopjcn  23612  indishmph  23754  tsmsxplem2  24110  rrx0el  25366  dchrfi  27234  ac6mapd  32712  elmaprd  32769  fcobij  32809  rmfsupp2  33331  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnlem4  33338  elrgspnsubrunlem2  33341  elrgspnsubrun  33342  linds2eq  33473  elrspunidl  33520  lbsdiflsp0  33803  fedgmullem1  33806  fedgmullem2  33807  fedgmul  33808  zarcmplem  34058  mbfmcst  34436  1stmbfm  34437  2ndmbfm  34438  mbfmco  34441  sibfof  34517  satfv1lem  35575  ex-sategoelel  35634  ex-sategoelelomsuc  35639  aks6d1c1  42480  aks6d1c2lem4  42491  aks6d1c5lem0  42499  aks6d1c5  42503  aks6d1c6lem1  42534  aks6d1c6lem2  42535  frlmfielbas  42864  fsuppind  42942  fsuppssindlem2  42944  fsuppssind  42945  mhpind  42946  mapco2g  43065  cantnfub  43672  tfsconcatrev  43699  ofoafg  43705  ofoafo  43707  rfovcnvf1od  44354  fsovfd  44362  fsovcnvlem  44363  dssmapnvod  44370  clsk3nimkb  44390  ntrelmap  44475  clselmap  44477  k0004lem2  44498  elmapsnd  45556  mapss2  45557  unirnmap  45560  inmap  45561  difmapsn  45564  unirnmapsn  45566  fourierdlem14  46473  fourierdlem15  46474  fourierdlem81  46539  fourierdlem92  46550  rrnprjdstle  46653  subsaliuncllem  46709  hoidmvlelem3  46949  ovolval2lem  46995  ovolval4lem2  47002  ovolval5lem2  47005  ovnovollem1  47008  smfmullem4  47146  fprmappr  48699  el0ldep  48820  naryfvalelfv  48986  fv1arycl  48991  1arymaptf  48995  2arymaptfo  49008