Theorem elmapdd 8782

Description: Deduction associated with elmapd 8781. (Contributed by SN, 29-Jul-2024.)

Hypotheses

Ref	Expression
elmapdd.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)
elmapdd.b	⊢ (𝜑 → 𝐵 ∈ 𝑊)
elmapdd.c	⊢ (𝜑 → 𝐶:𝐵⟶𝐴)

Assertion

Ref	Expression
elmapdd	⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑m 𝐵))

Proof of Theorem elmapdd

Step	Hyp	Ref	Expression
1		elmapdd.c	. 2 ⊢ (𝜑 → 𝐶:𝐵⟶𝐴)
2		elmapdd.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3		elmapdd.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
4	2, 3	elmapd 8781	. 2 ⊢ (𝜑 → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))
5	1, 4	mpbird 257	1 ⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑m 𝐵))

Syntax hints:   → wi 4   ∈ wcel 2114  ⟶wf 6489  (class class class)co 7361   ↑_m cmap 8767

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 5232  ax-pow 5303  ax-pr 5371  ax-un 7683

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 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-map 8769

This theorem is referenced by:  psdcl  22140  mhmcompl  22358  mhmcoaddmpl  22359  elrgspnlem1  33321  elrgspnlem2  33322  elrgspnlem3  33323  elrgspnlem4  33324  elrgspnsubrunlem1  33326  elrgspnsubrunlem2  33327  elrspunsn  33507  1arithidom  33615  extvfvvcl  33697  extvfvcl  33698  mplmulmvr  33701  evlscaval  33702  evlextv  33704  mplvrpmlem  33705  mplvrpmfgalem  33706  mplvrpmga  33707  mplvrpmmhm  33708  mplvrpmrhm  33709  psrmonprod  33714  mplmonprod  33716  esplyfval0  33726  esplylem  33728  esplympl  33729  esplyfv1  33731  esplyfvaln  33736  esplyind  33737  esplyindfv  33738  esplyfvn  33739  vietalem  33741  vieta  33742  ply1degltdimlem  33785  fldextrspunlsplem  33836  fldextrspunlsp  33837  hashnexinj  42584  mapcod  42699  mhmcopsr  43009  mhmcoaddpsr  43010  evlsbagval  43019  selvcllem5  43032  selvvvval  43035  evlselv  43037  mhphf  43047  dvnprodlem1  46395