Theorem elmapdd 8841

Description: Deduction associated with elmapd 8840. (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 8840	. 2 ⊢ (𝜑 → (𝐶 ∈ (𝐴 ↑m 𝐵) ↔ 𝐶:𝐵⟶𝐴))
5	1, 4	mpbird 260	1 ⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑m 𝐵))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ⟶wf 6529  (class class class)co 7414   ↑_m cmap 8827

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 2732  ax-sep 5251  ax-pow 5330  ax-pr 5398  ax-un 7737

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7417  df-oprab 7418  df-mpo 7419  df-map 8829

This theorem is used by:  s3rex  15022  s3rexrd  15023  mhmcompl  22338  mhmcoaddmpl  22340  selvcllem5  22356  selvvvval  22359  psdcl  22390  elrgspnlem1  33683  elrgspnlem2  33684  elrgspnlem3  33685  elrgspnlem4  33686  elrgspnsubrunlem1  33688  elrgspnsubrunlem2  33689  elrspunsn  33858  1arithidom  33948  0mplrim  34025  selvascl  34028  selvply1rhmlema  34029  selvply1rhmlemb  34030  selvply1rhmlem1  34031  selvply1rhmlem2  34032  selvply1rhmlem4  34034  selvply1rhm0  34037  extvfvcl  34047  mplmulmvr  34050  evlscaval  34051  evlextv  34053  mplvrpmlem  34054  mplvrpmfgalem  34055  mplvrpmga  34056  mplvrpmmhm  34057  mplvrpmrhm  34058  psrmonprod  34063  mplmonprod  34065  esplyfval0  34075  esplylem  34077  esplympl  34078  esplyfv1  34080  esplyfvaln  34085  esplyind  34086  esplyindfv  34087  esplyfvn  34088  vietalem  34090  vieta  34091  ply1degltdimlem  34133  fldextrspunlsplem  34184  fldextrspunlsp  34185  hashnexinj  42995  mapcod  43111  mhmcopsr  43427  mhmcoaddpsr  43428  evlsbagval  43433  evlselv  43436  mhphf  43444  dvnprodlem1  46775