Theorem elmapd 8888

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2147  ⟶wf 6554  (class class class)co 7443   ↑_m cmap 8875

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pow 5331  ax-pr 5395  ax-un 7775

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-map 8877

This theorem is used by:  elmapdd  8889  elmaprdOLD  8899  mapfset  8900  mapfoss  8902  elmapssres  8922  elmapresaun  8936  mapsnd  8942  mapss  8945  ralxpmap  8952  mapen  9188  mapunen  9193  mapfienlem3  9426  mapfien  9427  cantnfs  9694  acni  10151  infmap2  10322  fin23lem32  10449  iundom2g  10651  wunf  10839  hashf1lem2  14628  prdsplusg  17658  prdsmulr  17659  prdsvsca  17660  elsetchom  18285  setcco  18287  elestrchom  18331  estrcco  18333  funcsetcestrclem7  18364  elefmndbas  19098  isga  19535  symgbasmap  19621  frlmvplusgvalc  22103  frlmplusgvalb  22105  frlmvscavalb  22106  evls1sca  22671  mamures  22742  mat1dimmul  22821  1mavmul  22893  mdetunilem9  22965  cnpdis  23641  xkopjcn  24005  indishmph  24147  tsmsxplem2  24503  rrx0el  25749  dchrfi  27612  ac6mapd  33289  fcobij  33382  rmfsupp2  33868  elrgspnlem1  33873  elrgspnlem2  33874  elrgspnlem4  33876  elrgspnsubrunlem2  33879  elrgspnsubrun  33880  linds2eq  34006  elrspunidl  34048  lbsdiflsp0  34328  fedgmullem1  34331  fedgmullem2  34332  zarcmplem  34583  mbfmcst  34961  1stmbfm  34962  2ndmbfm  34963  mbfmco  34966  sibfof  35042  satfv1lem  36294  ex-sategoelel  36353  ex-sategoelelomsuc  36358  aks6d1c1  43358  aks6d1c2lem4  43369  aks6d1c5lem0  43377  aks6d1c5  43381  aks6d1c6lem1  43412  aks6d1c6lem2  43413  frlmfielbas  43760  fsuppind  43811  fsuppssindlem2  43813  fsuppssind  43814  mhpind  43815  mapco2g  43918  cantnfub  44515  tfsconcatrev  44542  ofoafg  44548  ofoafo  44550  rfovcnvf1od  45196  fsovfd  45204  fsovcnvlem  45205  dssmapnvod  45212  clsk3nimkb  45232  ntrelmap  45317  clselmap  45319  k0004lem2  45340  elmapsnd  46423  mapss2  46424  unirnmap  46426  inmap  46427  difmapsn  46430  unirnmapsn  46432  fourierdlem14  47336  fourierdlem15  47337  fourierdlem81  47402  fourierdlem92  47413  rrnprjdstle  47516  subsaliuncllem  47572  hoidmvlelem3  47812  ovolval2lem  47858  ovolval4lem2  47865  ovolval5lem2  47868  ovnovollem1  47871  smfmullem4  48009  fprmappr  49662  el0ldep  49783  naryfvalelfv  49949  fv1arycl  49954  1arymaptf  49958  2arymaptfo  49971