Theorem elmapd 8844

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2145  ⟶wf 6527  (class class class)co 7412   ↑_m cmap 8831

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7740

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6487  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-ov 7415  df-oprab 7416  df-mpo 7417  df-map 8833

This theorem is used by:  elmapdd  8845  elmaprdOLD  8855  mapfset  8856  mapfoss  8858  elmapssres  8878  elmapresaun  8892  mapsnd  8898  mapss  8901  ralxpmap  8908  mapen  9144  mapunen  9149  mapfienlem3  9383  mapfien  9384  cantnfs  9651  acni  10105  infmap2  10276  fin23lem32  10403  iundom2g  10605  wunf  10793  hashf1lem2  14581  prdsplusg  17609  prdsmulr  17610  prdsvsca  17611  elsetchom  18236  setcco  18238  elestrchom  18282  estrcco  18284  funcsetcestrclem7  18315  elefmndbas  19049  isga  19485  symgbasmap  19571  frlmvplusgvalc  22053  frlmplusgvalb  22055  frlmvscavalb  22056  evls1sca  22621  mamures  22692  mat1dimmul  22771  1mavmul  22843  mdetunilem9  22915  cnpdis  23591  xkopjcn  23955  indishmph  24097  tsmsxplem2  24453  rrx0el  25699  dchrfi  27564  ac6mapd  33199  fcobij  33294  rmfsupp2  33780  elrgspnlem1  33785  elrgspnlem2  33786  elrgspnlem4  33788  elrgspnsubrunlem2  33791  elrgspnsubrun  33792  linds2eq  33918  elrspunidl  33960  lbsdiflsp0  34240  fedgmullem1  34243  fedgmullem2  34244  fedgmul  34245  zarcmplem  34495  mbfmcst  34874  1stmbfm  34875  2ndmbfm  34876  mbfmco  34879  sibfof  34955  satfv1lem  36096  ex-sategoelel  36155  ex-sategoelelomsuc  36160  aks6d1c1  43134  aks6d1c2lem4  43145  aks6d1c5lem0  43153  aks6d1c5  43157  aks6d1c6lem1  43188  aks6d1c6lem2  43189  frlmfielbas  43532  fsuppind  43580  fsuppssindlem2  43582  fsuppssind  43583  mhpind  43584  mapco2g  43678  cantnfub  44281  tfsconcatrev  44308  ofoafg  44314  ofoafo  44316  rfovcnvf1od  44963  fsovfd  44971  fsovcnvlem  44972  dssmapnvod  44979  clsk3nimkb  44999  ntrelmap  45084  clselmap  45086  k0004lem2  45107  elmapsnd  46161  mapss2  46162  unirnmap  46164  inmap  46165  difmapsn  46168  unirnmapsn  46170  fourierdlem14  47075  fourierdlem15  47076  fourierdlem81  47141  fourierdlem92  47152  rrnprjdstle  47255  subsaliuncllem  47311  hoidmvlelem3  47551  ovolval2lem  47597  ovolval4lem2  47604  ovolval5lem2  47607  ovnovollem1  47610  smfmullem4  47748  fprmappr  49401  el0ldep  49522  naryfvalelfv  49688  fv1arycl  49693  1arymaptf  49697  2arymaptfo  49710