Theorem elmapd 8846

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2146  ⟶wf 6539  (class class class)co 7423   ↑_m cmap 8833

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-pow 5341  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428  df-map 8835

This theorem is used by:  elmapdd  8847  mapfset  8856  mapfoss  8858  elmapssres  8873  elmapresaun  8887  mapsnd  8893  mapss  8896  ralxpmap  8903  mapen  9139  mapunen  9144  mapfienlem3  9377  mapfien  9378  cantnfs  9645  acni  10048  infmap2  10219  fin23lem32  10346  iundom2g  10542  wunf  10730  hashf1lem2  14513  prdsplusg  17536  prdsmulr  17537  prdsvsca  17538  elsetchom  18163  setcco  18165  elestrchom  18209  estrcco  18211  funcsetcestrclem7  18242  elefmndbas  18963  isga  19392  symgbasmap  19478  frlmvplusgvalc  21954  frlmplusgvalb  21956  frlmvscavalb  21957  evls1sca  22520  mamures  22591  mat1dimmul  22670  1mavmul  22742  mdetunilem9  22814  cnpdis  23487  xkopjcn  23850  indishmph  23992  tsmsxplem2  24348  rrx0el  25594  dchrfi  27456  ac6mapd  33005  elmaprd  33062  fcobij  33102  rmfsupp2  33588  elrgspnlem1  33593  elrgspnlem2  33594  elrgspnlem4  33596  elrgspnsubrunlem2  33599  elrgspnsubrun  33600  linds2eq  33725  elrspunidl  33767  lbsdiflsp0  34047  fedgmullem1  34050  fedgmullem2  34051  fedgmul  34052  zarcmplem  34302  mbfmcst  34681  1stmbfm  34682  2ndmbfm  34683  mbfmco  34686  sibfof  34762  satfv1lem  35875  ex-sategoelel  35934  ex-sategoelelomsuc  35939  aks6d1c1  42924  aks6d1c2lem4  42935  aks6d1c5lem0  42943  aks6d1c5  42947  aks6d1c6lem1  42978  aks6d1c6lem2  42979  frlmfielbas  43315  fsuppind  43363  fsuppssindlem2  43365  fsuppssind  43366  mhpind  43367  mapco2g  43486  cantnfub  44089  tfsconcatrev  44116  ofoafg  44122  ofoafo  44124  rfovcnvf1od  44771  fsovfd  44779  fsovcnvlem  44780  dssmapnvod  44787  clsk3nimkb  44807  ntrelmap  44892  clselmap  44894  k0004lem2  44915  elmapsnd  45962  mapss2  45963  unirnmap  45965  inmap  45966  difmapsn  45969  unirnmapsn  45971  fourierdlem14  46876  fourierdlem15  46877  fourierdlem81  46942  fourierdlem92  46953  rrnprjdstle  47056  subsaliuncllem  47112  hoidmvlelem3  47352  ovolval2lem  47398  ovolval4lem2  47405  ovolval5lem2  47408  ovnovollem1  47411  smfmullem4  47549  fprmappr  49166  el0ldep  49287  naryfvalelfv  49453  fv1arycl  49458  1arymaptf  49462  2arymaptfo  49475